CADP demos README

This README file from the CADP distribution has been augmented with hypertext links to the README files for each demonstration. The demo descriptions have been annotated with notes in HTML format.

-- CAESAR/ALDEBARAN DISTRIBUTION PACKAGE
-- Hubert Garavel (C) CNRS/IMAG and INRIA
-- This software is subject to copyright restrictions defined in 
-- the document "Contrat de mise a` disposition de logiciels"

This directory contains various examples that explain how CAESAR, 
CAESAR.ADT and ALDEBARAN can be used. More details are given in
demo_*/:READ_ME files.

The examples are listed below:

	- demo_01 : alternating bit without data part 
		    [Hubert Garavel and Radu Mateescu]
		    Tools used: CAESAR, ALDEBARAN, EVALUATOR, XTL

demo_01

Basic LOTOS only, so it does not require a .h file (a concrete implementation in C of the abstract data types defined in the LOTOS source text).
Processes only. No data exchange.
caesar -aldebaran outputs a finite state automaton.
aldebaran can reduce it with strong equivalence, observational equivalence, or safety equivalence. It can also compare a specification with a simpler one by comparing their graphs.
evaluator can check a property stated in mu-calculus against a binary coded graph or open format.
xtl can also check a property stated in XTL.

	- demo_02 : alternating bit with data part 
		    [Hubert Garavel and Radu Mateescu]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, EVALUATOR, XTL

demo_02

The number of possible messages is defined in BITALT.t, an auxiliary file. The .t files are used by caesar.adt.
Processes only. Data exchanged at gates.
This example doesn't seem to need .f files.
Has a library BITALT.lib to go with BITALT.t.
Uses full LOTOS with data values. A .h file is not given, so it must be generated by one of the tools, namely caesar.adt.
Then caesar uses the .h file and -aldebaran option to generate a finite state automaton.
aldebaran reduces it with strong or observational equivalence. It can also compare the graph against a simpler one. It can also compare the graph against one with a known error.
evaluator can check a property stated in mu-calculus against a binary coded graph or open format.
xtl can also check a property stated in XTL.
The demonstrated property depends on the number of possible messages, which is defined in BITALT.t.

	- demo_03 : alternating bit with data part 
		    [Juan Quemada et al.]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN

demo_03

The number of possible messages is defined in DATALINK.t, an auxiliary file. The .t files are used by caesar.adt.
This example doesn't seem to need .f files. Has a library DATALINK.lib to go with DATALINK.t.
Uses full LOTOS with data values. A .h file is not given, so it must be generated by one of the tools, namely caesar.adt.
Then caesar uses the .h file and -aldebaran option to generate a finite state automaton.
aldebaran reduces it with safety or observational equivalence. It can also compare the graph against a simpler one. It can also copmare the graph against one with a known error, issuing diagnostic messages to help understand the reason for the error.

	- demo_04 : systolic arrays for convolution product 
		    [Hubert Garavel]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN

demo_04

Introduction of .f files, apparently symbolic implementations for abstract data types.
EXP.f, EXP.t, EXP.lib files all go together.
No .h file is given, so it must be generated by caesar.adt first. Then caesar -aldebaran is run to create the finite state automaton.
The examples can be reduced with observational equivalence.

	- demo_05 : linked list (only data types) 
		    [Hubert Garavel] 
		    Tools used: CAESAR.ADT

demo_05

caesar.adt translates data types in the LOTOS specification into equivalent C types and functions, creating a .h file.
The user.c file can directly test the abstract data type definitions (what about when you need to create your own .f files, how could you prove they were the same as your LOTOS specification?).
Doesn't seem to need a .t, .f, or .lib file. Why: because it doesn't need them or because they are taken care of with the BOOLEAN and NATURAL libraries included?

	- demo_06 : boolean array (only data types)
		    [Hubert Garavel]
		    Tools used: CAESAR.ADT, CAESAR

demo_06

Doesn't seem to need .t, .f, .lib files.
.h file not given, is produced by caesar.adt
README says it's similar to list in demo_05 because it takes advantage of "control part" of LOTOS without having to write any C code by hand, unless they were implying that the list in demo_05 DID have to write code by hand.
The sed scripts in the Makefile erase everything except the values emitted at the PRINT gate.

	- demo_07 : car overtaking protocol 
		    [P. Ernberg, L. Fredlund, B. Jonsson (SICS)]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, OPEN/CAESAR

demo_07

example of hiding and renaming gates
doesn't have .t, .f, .lib, .h files
comparision using safety equivalence on-the-fly
the properties are expressed as LTSs
open/caesar can be used with the simulator or xsimulator

	- demo_08 : rel/REL protocol 
		    [Laurent Mounier]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, OPEN/CAESAR

demo_08

uses a lot of memory
full LOTOS with values
has a .lib file and .hide file
doesn't have .t, .f, .h files
compare LTSs describing causality with respect to tau.* bisimulation or safety equivalence
scan execution sequences leading to deadlocks with terminator (this tool may not find all deadlocks)
causality properties expressed as LTSs

	- demo_09 : INRES protocol 
		    [Ana Cavalli and her research group at INT]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, OPEN/CAESAR

demo_09

Message Sequence Charts
guarded transitions in .lotos files
has .lib files, doesn't have .t, .f, .h files
introduces .seq files (describe allowed execution sequences)
detect deadlocks using caesar/open and terminator
compare LTSs for service and protocol with respect to safety equivalence or safety preorder (the service is not safety equivalent to the protocol, aldebaran gives an example sequence)
checking the sequences with exhibitor (displays the sequence found which satisfies the pattern in the .seq file)
simulate interactively with simulator or xsimulator

	- demo_10 : alternating bit with data part, same as demo_02
		    but tackled compositionally 
		    [Laurent Mounier and Hubert Garavel]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN

demo_10

has .t, .lib files
introduces .exp files (describes a system or network of communicating LTSs, expanded on-the-fly)
use aldebaran to check for deadlocks (sinks)
use aldebaran to check for livelocks (tau circuits)
can reduce or compare with branching bisimulation
compositional verification

	- demo_11 : rel/REL protocol with data part, same as demo_08
		    but tackled compositionally 
		    [Laurent Mounier and Hubert Garavel]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN

demo_11

reduction makefile takes very long time
has .lib, .t, .exp, .hide files
services to compare are expressed as LTSs
more feedback for deadlocks needed: does the tool support?
compositional verification

	- demo_12 : Message Authentication Algorithm, ISO standard 8731
		    (pure data types) formally described in LOTOS by 
		    Harold Munster (NPL) 
		    [Hubert Garavel, Philippe Turlier and Radu Mateescu]
		    Tools used: CAESAR.ADT

demo_12

has .t, .f files
has main.c program to interact with user, test the maa

	- demo_13 : a collection of BCG graphs to be displayed using BCG_DRAW
		    [Radu Mateescu and Hubert Garavel]
		    Tools used: BCG_DRAW

demo_13

graphs are extremely dense (almost black in areas)
.aut files and their corresponding .bcg files (just the .bcg ones are drawn)
can these be reduced with other options? yes:
- aldebaran -smin D1.aut
- aldebaran -omin D1.aut
- aldebaran -pmin D1.aut
- aldebaran -imin D1.aut

(skip to 19) 

	- demo_14 : Plain Old Telephony System (POTS), specified in LOTOS
		    by Patrick Ernberg (SICS)
		    [Laurent Mounier]
		    Tools used: CAESAR, ALDEBARAN 

	- demo_15 : Plain Old Telephony System (POTS), specified in LOTOS
		    by Patrick Ernberg (SICS)
		    [Laurent Mounier]
		    Tools used: OPEN/CAESAR, EVALUATOR

	- demo_16 : Philips' Bounded Retransmission Protocol specified in
		    LOTOS and verified using ACTL temporal logic formulas
		    [Radu Mateescu]
		    Tools used: CAESAR, ALDEBARAN, XTL

	- demo_17 : Distributed Leader Election Algorithms specified in LOTOS
		    [Hubert Garavel and Laurent Mounier]
		    Tools used: CAESAR, ALDEBARAN

	- demo_18 : Transit Node message router specified in LOTOS
		    [Laurent Mounier]
		    Tools used: CAESAR, ALDEBARAN, EXP.OPEN

(resume)

	- demo_19 : Production Cell case-study, where a LOTOS description
		    is used to control a metal plant simulated by a Tcl/Tk
		    animated interface 
		    [Hubert Garavel and Mark Jorgensen]
		    Tools used: EXEC/CAESAR

demo_19

simulation with Tcl/Tk interface
has driver.c and main.c code files
has .t and .f files
cell is a LOTOS file with macro descriptions to be expanded

(stop)

	- demo_20 : rel/REL protocol (see demo_08 and demo_11) but with
		    four stations verified compositionally
		    [Laurent Mounier]
		    Tools used: OPEN/CAESAR, PROJECTOR, EVALUATOR

	- demo_21 : Peterson's mutual exclusion algorithm specified in
		    LOTOS and verified using LTAC temporal logic formulas
		    [Radu Mateescu]
		    Tools used: CAESAR, XTL

	- demo_22 : Dekker's mutual exclusion algorithm specified in
		    LOTOS and verified using LTAC temporal logic formulas
		    [Radu Mateescu]
		    Tools used: CAESAR, XTL

	- demo_23 : IEEE 1394 high performance serial bus ("Firewire")
		    specified in LOTOS
		    [Mihaela Sighireanu and Radu Mateescu]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, BCG, XTL

	- demo_24 : CO4 protocol for distributed knowledge bases specified 
		    in LOTOS
		    [Charles Pecheur]
		    Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, EXHIBITOR, 
		    TERMINATOR, BCG_DRAW

	- demo_25 : Cluster File System (CFS) specified in LOTOS
		    [Charles Pecheur]
		    Tools used: CAESAR, ALDEBARAN, EXP.OPEN, XTL