Repository

The models presented during the MARS workshops are made available on a perennial form, so that they can be used by others and that the experiments are reproducible. The list of models is expected to grow as time passes, and to be as diverse as possible. The repository of models is hosted by Inria (France).

List of all models

Description Formalism(s)/Tool(s) Event
020 CBTC Automatic Train Supervision System UMC; Promela (Spin); NuSMV/nuXmv; mCRL2; CPN tools; FDR4; ProB; LNT (CADP); TLA toolbox; ProB; Uppaal; ProB MARS'18
019 Tera-Scale ARchitecture (TSAR) Promela (Spin); Divine (DiVine, ITS-tools); ITS-tools MARS'18
018 LTS Handshake Model LNT (CADP) MARS'18
017 Robotic Cell Injection Discrete-Time Markov Chain (PRISM) MARS'17
016 Production Cell LNT (CADP); LOTOS (CADP) MARS'17
015 A Model-Derivation Framework for Software Analysis Uppaal MARS'17
014 Emergency Power Supply BDMP(KB3) MARS'17
013 AUTOSAR Erlang QuickCheck MARS'17
012 Message Authenticator Algorithm REC tool; AProVE tool; Clean; Haskell; LNT (CADP); LOTOS (CADP); Maude; mCRL2; OCaml; Opal; Rascal; Scala; Standard ML; Stratego/XT; Tom; LOTOS (CADP); LNT (CADP) MARS'17
MARS'18
011 IEEE 802.15.4 TCSH MAC mCRL2 tool suite MARS'17
010 Memory Access and Interrupts Isabelle/HOL MARS'17
009 B.A.T.M.A.N. Uppaal MARS'17
008 Fragmentation and Reassembly for CAN AWN MARS'17
007 Stream Control Transmission Protocol Uppaal MARS'17
006 DES Standard LNT (CADP); LOTOS (CADP) MARS'15
005 Bitcoin Protocol Uppaal MARS'15
004 Caches and Pipelines Uppaal MARS'15
003 Self-Balancing Unicycles SpaceEx; Mathematica MARS'15
002 eChronos Isabelle/HOL MARS'15
001 Bilby File System Isabelle/HOL MARS'15

All models are licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.

© 2015–2018, Last Update April 13, 2018.