A number of commented demos are included in the CADP package and also available on-line from http://cadp.inria.fr/ftp/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, Laurent Mounier, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, EVALUATOR, SVL, XTL
demo_03: (left temporarily empty)
demo_04:
Systolic arrays for convolution product
Hubert Garavel, Reyhane Falanji, and Florian Gallay
Tools used: CAESAR, CAESAR.ADT, BCG_CMP, BCG_MIN, LNT2LOTOS, SVL
demo_05:
Airplane-ground communication protocol
Damien Thivolle, Hubert Garavel, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, EVALUATOR, EXP.OPEN,
LNT2LOTOS, PROJECTOR, SVL
demo_06:
Transport Layer Security (TLS 1.3) handshake protocol
Lina Marsso
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, LNT2LOTOS, SVL, TGV
demo_07:
Car overtaking protocol
Patrik Ernberg, Lars-Ake Fredlund, Bengt Jonsson, Almer Bolatov, and Hubert Garavel
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BISIMULATOR, LNT2LOTOS, OPEN/CAESAR, SVL
demo_08:
rel/REL atomic multicast protocol
Laurent Mounier, Hubert Garavel, Frédéric Lang, and Radu Mateescu
Tools used: BCG, BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, EVALUATOR, LNT2LOTOS, OPEN/CAESAR, PROJECTOR, SVL
demo_09:
INRES protocol
Ana Cavalli et al., Hubert Garavel, Séverine Simon, Almer Bolatov
Tools used: CAESAR, CAESAR.ADT, BISIMULATOR, LNT2LOTOS, OPEN/CAESAR, SVL, TGV
demo_10:
Mutual exclusion protocols for shared memory
Radu Mateescu and Wendelin Serwe
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BCG_STEADY, CUNCTATOR, EVALUATOR, LNT2LOTOS, PROJECTOR, SVL
demo_11:
Dynamic Task Dispatcher
Etienne Lantreibecq and Wendelin Serwe
Tools used: BCG_MIN, EVALUATOR 4.0, LNT.OPEN, SVL
demo_12:
Message Authenticator Algorithm, ISO standard 8731-2 formally described by Harold Munster (NPL)
Hubert Garavel, Philippe Turlier, Radu Mateescu, Wendelin Serwe, and Lina Marsso
Tools used: LNT2LOTOS, 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 by Patrick Ernberg (SICS)
Laurent Mounier, Radu Mateescu, Frédéric Lang, and Hubert Garavel
Tools used: LNT2LOTOS, CAESAR, CAESAR.ADT, BCG_MIN, OPEN/CAESAR, BISIMULATOR, EVALUATOR, SVL
demo_15:
Erlangen mainframe
Hubert Garavel
Tools used: BCG_MIN, BCG_STEADY, BCG_TRANSIENT, CAESAR, CAESAR.ADT, LNT2LOTOS, SVL, XTL
demo_16:
Philips' Bounded Retransmission Protocol verified using ACTL temporal logic formulas
Radu Mateescu, Hubert Garavel, Julien Jacques Maurer, and Jose-Ignacio Requeno
Tools used: LNT2LOTOS, CAESAR, CAESAR.ADT, BCG, BISIMULATOR, SVL, XTL
demo_17:
Token-ring leader election algorithms
Hubert Garavel, Laurent Mounier, Frédéric Lang, and Wendelin Serwe
Tools used: CAESAR, CAESAR.ADT, LNT.OPEN, BCG_MIN, OPEN/CAESAR, BISIMULATOR, EXHIBITOR, TERMINATOR, SVL
demo_18:
Transit Node message router
Laurent Mounier, Frédéric Lang, Julian Jacques Maurer, Alexander Graf-Brill, and Hubert Garavel
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, EXP.OPEN, LNT2LOTOS, SVL
demo_19:
Production Cell case-study, where a formal description is used to control a metal plant simulated by a Tcl/Tk animated interface
Hubert Garavel, Mark Jorgensen, and Wendelin Serwe
Tools used: CAESAR, CAESAR.ADT, EXEC/CAESAR, LNT2LOTOS
demo_20: (left temporarily empty)
demo_21:
Peterson's mutual exclusion algorithm verified using temporal logic formulas
Radu Mateescu, Frédéric Lang, Hubert Garavel, and Gianluca Barbon
Tools used: CAESAR, CAESAR.ADT, EVALUATOR, LNT2LOTOS, SVL, XTL
demo_22:
Dekker's mutual exclusion algorithm verified using temporal logic formulas
Radu Mateescu, Frédéric Lang, Hubert Garavel, and Gianluca Barbon
Tools used: CAESAR, CAESAR.ADT, EVALUATOR, LNT2LOTOS, SVL, XTL
demo_23:
IEEE 1394 high performance serial bus ("Firewire")
Mihaela Sighireanu, Radu Mateescu, Frédéric Lang, Marck-Edward Kemeh, Oussama Oulkaid, and Hubert Garavel
Tools used: CAESAR, CAESAR.ADT, BCG, LNT2LOTOS, SVL, XTL
demo_24:
CO4 protocol for distributed knowledge bases
Charles Pecheur, Frédéric Lang, Vincent Ribot, Jolahn Vaudey, and Hubert Garavel
Tools used: CAESAR, CAESAR.ADT, LNT2LOTOS, EXHIBITOR, TERMINATOR, BCG_DRAW, SVL
demo_25:
Cluster File System (CFS)
Charles Pecheur, Frédéric Lang, Marck-Edward Kemeh, Oussama Oulkaid, and Hubert Garavel
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, EXP.OPEN, SVL, XTL
demo_26:
Invoicing case study
Mihaela Sighireanu, Ken Turner, Frédéric Lang, Reyhane Falanji, Florian Gallay, and Hubert Garavel
Tools used: BCG_CMP, BCG_MIN, CAESAR, CAESAR.ADT, LNT2LOTOS, SVL, XTL
demo_27:
HAVi (Home Audio-Video) leader election protocol
Judi Romijn, Radu Mateescu, Frédéric Lang, Hubert Garavel, Reyhane Falanji, and Florian Gallay
Tools used: BCG_MIN, BCG_CMP, CAESAR, CAESAR.ADT, EXP.OPEN, LNT2LOTOS, SVL, XTL
demo_28:
Directory-based cache coherency protocol
Massimo Zendri, Hubert Garavel, Frédéric Lang, Abderahman Kriouile, and Wendelin Serwe
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, LNT2LOTOS, SVL
demo_29:
Dynamic reconfiguration protocol for mobile agents
Manuel Aguilar Cornejo, Hubert Garavel, Radu Mateescu, and Noel de Palma
Tools used: BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, EVALUATOR, LNT2LOTOS, SVL
demo_30:
Hubble space telescope lifetime
Holger Hermanns, Christophe Joubert, Hubert Garavel, and Wendelin Serwe
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BCG_TRANSIENT, LNT2LOTOS, SVL
demo_31:
SCSI-2 bus arbitration protocol
Hubert Garavel, Holger Hermanns, Radu Mateescu, Christophe Joubert, David Champelovier, and Frédéric Lang
Tools used: CAESAR, CAESAR.ADT, BCG_MIN, BCG_STEADY, DETERMINATOR, EVALUATOR, LNT2LOTOS, SVL
demo_32:
Sequentially consistent, distributed cache memory
Susanne Graf, Wendelin Serwe, Abderahman Kriouile, and Hubert Garavel
Tools used: BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, LNT2LOTOS, SVL
demo_33:
Randomized binary distributed consensus protocol
Frédéric Tronel, Frédéric Lang, Hubert Garavel, Reyhane Falanji, and Florian Gallay
Tools used: BCG_GRAPH, BCG_MIN, CAESAR, CAESAR.ADT, LNT2LOTOS, PROJECTOR, SVL
demo_34:
Computer integrated manufacturing (CIM) architecture
Radu Mateescu, Heinrich Ody, and Hubert Garavel
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, EVALUATOR, LNT2LOTOS, SVL
demo_35:
Distributed summation algorithm using "n among m" synchronization
Frédéric Lang, Marius Hollinger, and Hubert Garavel
Tools used: BCG_MIN, CAESAR, CAESAR.ADT, EXP.OPEN, LNT2LOTOS, SVL
demo_36:
Distributed Eratosthenes sieve
Frédéric Lang, Hubert Garavel, Gianluca Barbon, and Radu Mateescu
Tools used: BCG_LABELS, BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, EVALUATOR4, EXP.OPEN, LNT2LOTOS, SVL
demo_37:
ODP (Open Distributed Processing) trader
Frédéric Lang, Marius Hollinger, and Hubert Garavel
Tools used: BCG_MIN, BISIMULATOR, CAESAR.ADT, CAESAR, EXP.OPEN, LNT2LOTOS, 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, LNT2LOTOS, PROJECTOR, SVL
demo_39:
Turntable system for drilling products
Radu Mateescu, Marius Hollinger, and Hubert Garavel
Tools used: BCG_MIN, BCG_STEADY, BISIMULATOR, CAESAR, CAESAR.ADT, DETERMINATOR, EVALUATOR, LNT2LOTOS, 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