What is CADP?
Home Page Tools Overview Current Status
Installation
How to obtain CADP? Usage Statistics Issues & Patches
Documentation
Tutorials Publications Manual Pages Demo Examples FAQ
CADP Newsletters
Nr. 1 - Dec. 1996 Nr. 2 - Jun. 1997 Nr. 3 - Sep. 1997 Nr. 4 - Jan. 1999 Nr. 5 - Jul. 2001 Nr. 6 - Apr. 2007
CADP Community
Forum Education & Training Case Studies Research Tools
CADP Resources
VLTS Benchmarks Other Resources
About CADP
Contributors

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:

• An explanatory file (named =READ_ME.txt)
• A tar-compressed archive (named demo_xx.tar.Z) for Unix users
• A zip archive (named demo_xx.zip) for PC/Windows and Unix users

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

---

Version 1.25 last updated on 12/04/10 09:24:11

---

Back to the VASY Home Page