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
021 Distributed Integrated Modular Avionics (DIMA) Uppaal MARS'18
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
015 A Model-Derivation Framework for Software Analysis Uppaal MARS'17
010 Memory Access and Interrupts Isabelle/HOL MARS'17
018 TLS Handshake Model LNT (CADP) MARS'18
004 Caches and Pipelines Uppaal MARS'15
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
016 Production Cell LNT (CADP); LOTOS (CADP) MARS'17
013 AUTOSAR Erlang QuickCheck MARS'17
005 Bitcoin Protocol Uppaal MARS'15
006 DES Standard LNT (CADP); LOTOS (CADP) MARS'15
017 Robotic Cell Injection Discrete-Time Markov Chain (PRISM) MARS'17
002 eChronos Isabelle/HOL MARS'15
011 IEEE 802.15.4 TCSH MAC mCRL2 tool suite MARS'17
009 B.A.T.M.A.N. Uppaal MARS'17
021 Distributed Integrated Modular Avionics (DIMA) Uppaal MARS'18
007 Stream Control Transmission Protocol Uppaal MARS'17
001 Bilby File System Isabelle/HOL MARS'15
019 Tera-Scale ARchitecture (TSAR) Promela (Spin); Divine (DiVine, ITS-tools); ITS-tools MARS'18
003 Self-Balancing Unicycles SpaceEx; Mathematica MARS'15
014 Emergency Power Supply BDMP(KB3) MARS'17

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

© 2015–2018, Last Update October 15, 2018.