Contribution: ABP

A verification of the alternating bit protocol expressed in CBS

Authors

Description

Keywords

alternating bit protocol, process calculi, reactive systems, co inductive types, co induction

README

This directory contains developments based on a variant 
of Prasad's Calculus of Broadcasting Systems (CBS). For
a detailed description, see:


@INPROCEEDINGS{EG95a,
        AUTHOR             = {E. Gim\'enez},
        BOOKTITLE          = {Workshop on Types for Proofs and Programs},
        SERIES             = {LNCS},
        NUMBER             = {1158},
        PAGES              = {135-152},
        TITLE              = {An application of co-Inductive types in Coq: 
		               verification of the Alternating Bit Protocol},
        EDITORS            = {S. Berardi and M. Coppo},
        PUBLISHER          = {Springer-Verlag},
        YEAR               = {1995}
}

@PhdThesis{EG96,
  author = 	 {E. Gim\'enez},
  title = 	 {A Calculus of Infinite Constructions and its
                  application to the verification of communicating systems},
  school = 	 {Ecole Normale Sup\'erieure de Lyon},
  year = 	 {1996}
}

Warning: The contribution has been updated for the beta release of Coq
V6.1, so what is described in reference EG95a does not exactly
correspond to the contents of these directories. The proof is now
shorter and simpler.


Directory ABP/TRACES : 
======================

A verification of the alternating bit protocol expressed in CBS.
This proof is based on reasoning about the infinite tree of traces 
generated by the protocol.

	* File Processwc.v  : The axiomatisation of CBS and some useful 
                              properties about traces.

	* File Protocol.v   : The description of the alternating bit protocol
			      in CBS.

	* File Hypothesis.v : The hypothesis assumed for modeling the problem.

	* File Lemmas.v     : Unfolding lemmas for the states of the protocol
			      and the inversion lemmas for the transition
			      relation.

	* Files It_Will_Happen.v, Determined.v and Correctness.v : The proof.


Directory ABP/BISIMULATION : 
===========================

A verification of the alternating bit protocol expressed in CBS (II).
This proof is based on the notion of bisimulation.

Directory INTERPRETER :
====================== 

Verification of an interpreter for CBS. 

	* File Process.v    :   The verification of the interpreter.

	* File raugh.v      :   The raugh program extracted by Coq.

	* File improved.gs  :   An improved version obtained form raugh.v

	* File interface.gs : A minimal interface to run the simulator 
                              in Gofer. 

	* File example.gs   : An example to be run with the interpreter.



In order to run the example you need Gofer's interpreter
(version 2.28). Concatenate the files improved.gs, interface.gs 
and example.gs into a single one. Call Gofer's interpreter
and load this file. To start the simulation, enter:

? (go decide system)

You may point to the process you want to schedule, and the 
simulator answers with the message transmitted by the
chosen process. In order to design the process to be 
schedule, enter one of these actions (in capital letters) :
-- LF : The left agent is talks and its message is lost. 
-- RF : The right agent talks and its message is lost.
-- LS : The left agent talks and succeeds its transmission. 
-- RS : The right agent talks and succeeds its transmission. 

You should obtain the stream of messages 0,1,2,3, etc. as
the trace of the process.

Available files