A number of commented demos are included in the CADP package and also available on-line from the VASY FTP server: ftp://ftp.inrialpes.fr/pub/vasy/demos. Each demo is organized as a directory containing various files, including:
These demos are listed below:
demo_01:
Alternating bit without data part
Hubert Garavel, Radu Mateescu, Séverine Simon, and Frédéric Lang
Tools used: CAESAR, BISIMULATOR, EVALUATOR, SVL, TGV, XTL
demo_02:
Alternating bit with data part
Hubert Garavel, Radu Mateescu, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, EVALUATOR, SVL, XTL
demo_03:
Alternating bit with data part
Juan Quemada et al.
Tools used: CAESAR, CAESAR.ADT, BISIMULATOR, SVL
demo_04:
Systolic arrays for convolution product
Hubert Garavel
Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, SVL
demo_05:
Linked list (data types only)
Hubert Garavel
Tools used: CAESAR.ADT
demo_06:
Boolean array (data types only)
Hubert Garavel
Tools used: CAESAR.ADT, CAESAR, SVL
demo_07:
Car overtaking protocol
P. Ernberg, L. Fredlund, B. Jonsson (SICS)
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, OPEN/CAESAR, SVL
demo_08:
rel/REL protocol
Laurent Mounier
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, OPEN/CAESAR, SVL
demo_09:
INRES protocol
Ana Cavalli et al., Hubert Garavel, Séverine Simon
Tools used: CAESAR, CAESAR.ADT, BISIMULATOR, OPEN/CAESAR, TGV
demo_10:
Alternating bit with data part, same as demo_02 but tackled compositionally
Laurent Mounier, Hubert Garavel, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, SVL
demo_11:
rel/REL protocol with data part, same as demo_08 but tackled compositionally
Laurent Mounier, Hubert Garavel, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, SVL
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_13:
Collection of BCG graphs to be displayed using BCG_DRAW
Radu Mateescu and Hubert Garavel
Tools used: BCG_DRAW
demo_14:
Plain Old Telephony System (POTS), specified in LOTOS by Patrick Ernberg (SICS)
Laurent Mounier and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, SVL
demo_15:
Plain Old Telephony System (POTS), specified in LOTOS by Patrick Ernberg (SICS)
Laurent Mounier, Radu Mateescu, and Frédéric Lang
Tools used: OPEN/CAESAR, EVALUATOR, SVL
demo_16:
Philips' Bounded Retransmission Protocol specified in LOTOS and verified using ACTL temporal logic formulas
Radu Mateescu
Tools used: CAESAR, CAESAR.ADT, BCG, BISIMULATOR, SVL, XTL
demo_17:
Distributed Leader Election Algorithms specified in LOTOS
Hubert Garavel, Laurent Mounier, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, EXHIBITOR, TERMINATOR, OPEN/CAESAR, SVL
demo_18:
Transit Node message router specified in LOTOS
Laurent Mounier and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, EXP.OPEN, SVL
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_20:
rel/REL protocol (see demo_08 and demo_11) but with four stations verified compositionally
Laurent Mounier, Radu Mateescu, and Frédéric Lang
Tools used: BCG, BISIMULATOR, CAESAR, CAESAR.ADT, EVALUATOR, OPEN/CAESAR, PROJECTOR, SVL
demo_21:
Peterson's mutual exclusion algorithm specified in LOTOS and verified using LTAC temporal logic formulas
Radu Mateescu
Tools used: CAESAR, EVALUATOR, SVL, XTL
demo_22:
Dekker's mutual exclusion algorithm specified in LOTOS and verified using LTAC temporal logic formulas
Radu Mateescu
Tools used: CAESAR, EVALUATOR, SVL, XTL
demo_23:
IEEE 1394 high performance serial bus ("Firewire") specified in LOTOS
Mihaela Sighireanu, Radu Mateescu, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG, SVL, XTL
demo_24:
CO4 protocol for distributed knowledge bases specified in LOTOS
Charles Pecheur and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, ALDEBARAN, EXHIBITOR, TERMINATOR, BCG_DRAW, SVL
demo_25:
Cluster File System (CFS) specified in LOTOS
Charles Pecheur, Frédéric Lang, and Hubert Garavel
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, EXP.OPEN, SVL, XTL
demo_26:
Invoicing case study specified in LOTOS
Mihaela Sighireanu, Ken Turner, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, SVL, XTL
demo_27:
HAVi (Home Audio-Video) leader election protocol
Judi Romijn, Radu Mateescu, and Frédéric Lang
Tools used: CAESAR, EXP.OPEN, BCG_MIN, SVL, XTL
demo_28:
Directory-based cache coherency protocol
Massimo Zendri, Hubert Garavel, and Frédéric Lang
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, SVL
demo_29:
Dynamic reconfiguration protocol for mobile agents
Manuel Aguilar Cornejo, Hubert Garavel, and Radu Mateescu
Tools used: BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, EVALUATOR, LNT2LOTOS, SVL
demo_30:
Hubble space telescope lifetime
Holger Hermanns, Christophe Joubert, and Hubert Garavel
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BCG_TRANSIENT, SVL
demo_31:
SCSI-2 bus arbitration protocol
Hubert Garavel, Holger Hermanns, Radu Mateescu, Christophe Joubert, and David Champelovier
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BCG_STEADY, DETERMINATOR, EVALUATOR, SVL
demo_32:
Sequentially consistent, distributed cache memory
Susanne Graf and Wendelin Serwe
Tools used: CAESAR, CAESAR.ADT, BISIMULATOR, BCG_MIN, SVL
demo_33:
Randomized binary distributed consensus protocol
Frédéric Tronel and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_GRAPH, BISIMULATOR, PROJECTOR, SVL
demo_34:
Computer integrated manufacturing (CIM) architecture
Radu Mateescu
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, EVALUATOR, SVL
demo_35:
Distributed summation algorithm using "n among m" synchronization
Frédéric Lang
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, EXP.OPEN, SVL
demo_36:
Distributed Erathostenes sieve
Frédéric Lang
Tools used: BCG_LABELS, BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, EXP.OPEN, SVL
demo_37:
ODP (Open Distributed Processing) trader
Frédéric Lang
Tools used: BCG_MIN, BISIMULATOR, CAESAR.ADT, CAESAR, EXP.OPEN, PROJECTOR, SVL
demo_38:
Asynchronous circuit for the DES (Data Encryption Standard)
Wendelin Serwe and Hubert Garavel
Tools used: BCG_MIN, BISIMULATOR, CAESAR.ADT, CAESAR, EXEC/CAESAR, EXP.OPEN, PROJECTOR, SVL
demo_39:
Turntable system for drilling products
Radu Mateescu
Tools used: BCG_MIN, BCG_STEADY, BISIMULATOR, CAESAR, CAESAR.ADT, DETERMINATOR, EVALUATOR, SVL
demo_40:
Web services for stock management and on-line book auction
Antonella Chirichiello, Gwen Salaun, and Wendelin Serwe
Tools used: CAESAR, CAESAR.ADT, EVALUATOR, SVL