What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

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:

• An explanatory file (named =READ_ME.txt)
• A tar-compressed archive (named demo_xx.tar.gz)
• A zip archive (named demo_xx.zip) with the same contents as the former

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, 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, EVALUATOR, 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, Wendelin Serwe, and Hubert Garavel
  Tools used: CAESAR, CAESAR.ADT, EVALUATOR, LNT2LOTOS, SVL

---

Version 1.102 last updated on 2024/12/10 18:51:35

---

Back to the CADP Home Page