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

no sort_icon Descriptionsort_icon Formalism(s)/Tool(s)sort_icon Eventsort_icon
029 Raft Distributed Consensus Protocol LNT (CADP) MARS'20
028 Electronic Control Unit (ECU) of an Electronic Power-Assisted Steering (EPAS) Unit Gamma MARS'20
027 Needle Steering Uppaal MARS'20
026 Aircraft Velocity Control System with Redundancy Mechanisms Promela (Spin) MARS'20
025 End-to-EndLatencies in Automotive Cyber-physical Systems MiniZinc MARS'20
024 OLSR version2 Routing Protocol AWN MARS'20
023 OSPF Routing Protocol AWN; Uppaal MARS'20
022 Asynchronous Circuit Dedicated to the Protection Against Physical Attacks LNT (CADP) MARS'20
021 Distributed Integrated Modular Avionics (DIMA) Uppaal MARS'18
020 CBTC Automatic Train Supervision System FDR4; Uppaal; NuSMV/nuXmv; LNT (CADP); Promela (Spin); CPN tools; UMC; TLA toolbox; ProB; mCRL2 MARS'18
019 Tera-Scale ARchitecture (TSAR) Promela (Spin); Divine (DiVine, ITS-tools); ITS-tools MARS'18
018 TLS Handshake Model LNT (CADP) MARS'18
017 Robotic Cell Injection Discrete-Time Markov Chain (PRISM) MARS'17
016 Production Cell LOTOS (CADP); LNT (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 AProVE tool; Scade; LOTOS (CADP); Scala; Lustre; Opal; Rascal; OCaml; Standard ML; Haskell; REC tool; Maude; Clean; Tom; Stratego/XT; LNT (CADP); mCRL2 MARS'17
MARS'18
MARS'20
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 LOTOS (CADP); LNT (CADP) MARS'15
005 Bitcoin Protocol Uppaal MARS'15
004 Caches and Pipelines Uppaal MARS'15
003 Self-Balancing Unicycles Mathematica; SpaceEx 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–2020, Last Update April 30, 2020.