Affiliated with the
European Joint Conferences on Theory and Practice of Software (ETAPS 2022)

Munich, Germany


The MARS workshops bring together researchers from different communities who are developing formal models of real systems in areas where complex models occur, such as networks, cyber-physical systems, hardware/software codesign, biology, etc. The motivation and aim for MARS stem from the following two observations:

  • Large case studies are essential to show that specification formalisms and modelling techniques are applicable to real systems, whereas many research papers only consider toy examples or tiny case studies.
  • Developing an accurate model of a real system takes a large amount of time, often months or years. In most scientific papers, however, salient details of the model need to be skipped due to lack of space, and to leave room for formal verification methodologies and results.

The MARS workshops aim at remedying these issues, emphasising modelling over verification, so as to retain lessons learnt from formal modelling, which are not usually discussed elsewhere. Examples are:

  • Which formalism was chosen, and why?
  • Which abstractions have been made, and why?
  • How were important characteristics of the system modelled?
  • Were there any complications while modelling the system?
  • Which measures were taken to guarantee the accuracy of the model?
  • How can different modelling approaches be compared on this system?

We thus invite papers that present formal models of real systems, which may lay the basis for future analysis and comparison.

In addition to the workshop proceedings, the formal models presented at the workshop will be archived in the MARS Repository, a growing, diverse collection of realistic benchmarks. The existence of this repository is a unique feature that makes MARS contributions available to the wider community, so that others can reproduce experiments, perform further analyses, and try the same case studies using different formal methods.


The following program comprises invited talks, presentations of MARS 2020 publications that had to be cancelled due to the pandemic situation, and talks of accepted papers of MARS 2022.
The location is room 00.08.036 in the 5608 building of TUM, Garching. Virtual attendants please log in to zoom.
8:45-9:00 Registration and Opening
9:00-10:00 Invited Talk I
Modeling the Raft Distributed Consensus Protocol in LNT (MARS'20)
     Hugues Evrard
10:00-10:30 Coffee Break
10:30-12:30 Formal Quantitative Modeling
Stateful to Stateless: Modelling Stateless Ethereum (MARS'22)
     Sandra Johnson, David Hyland-Wood, Anders Madsen, and Kerrie Mengersen
Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks (MARS'20)
     Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, and Marc Renaudin
Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing (MARS'22)
     Lina Marsso, Radu Mateescu, Lucie Muller, and Wendelin Serwe
Formal Modelling and Initial Analysis of the 4SECURail Case Study (MARS'22)
     Franco Mazzanti and Dimitri Belli
12:30-14:00 Lunch Break
14:00-15:00 Invited Talk II
Modest Models and Tools for Real Stochastic Timed Systems (MARS'22)
     Arnd Hartmanns
15:00-16:00 Protocol and Controller Modeling
Formalising the Optimised Link State Routing Protocol (MARS'20)
     Ryan Barry, Rob van Glabbeek, and Peter Höfner
Iterative Variable Reordering: Taming Huge System Families (MARS'20)
     Clemens Dubslaff, Andrey Morozov, Christel Baier, and Klaus Janschek
16:00-16:30 Coffee Break
16:30-17:50 Uppaal
Advanced Models for the OSPF Routing Protocol (MARS'20/22)
     Courtney Darville, Peter Höfner, Franc Ivankovic, and Adam Pam
Modeling R3 Needle Steering in Uppaal (MARS'20/22)
     Sascha Lehmann, Antje Rogalla, Maximilian Neidhardt, Anton Reinecke, Alexander Schlaefer, and Sibylle Schupp
17:50-18:00 Closing

Invited Talks

Modeling the Raft Distributed Consensus Protocol in LNT by Hugues Evrard (Google, London, UK)
Abstract. Consensus protocols are crucial for reliable distributed systems as they let them cope with network and server failures. For decades, most consensus protocols have been designed as variations of the seminal Paxos, yet in 2014 Raft was presented as a new, “understandable” protocol, meant to be easier to implement than the notoriously subtle Paxos family. Raft has since been used in various industrial projects, e.g. Hashicorp’s Consul or etcd (used by Google’s Kubernetes). The correctness of Raft is established via a manual proof, based on a TLA+ specification of the protocol. This presentation reports our experience in modeling Raft in the LNT process algebra. We found a couple of issues with the original TLA+ specification of Raft, which has been corrected since. More generally, this exercise offers a great opportunity to discuss how to best use the features of the LNT formal language and the associated CADP verification toolbox to model distributed protocols, including network and server failures.

Modest Models and Tools for Real Stochastic Timed Systems by Arnd Hartmanns (University Twente, The Netherlands)
Abstract. We depend on the safe, reliable, and timely operation of various cyber-physical systems ranging from smart grids to avionics components, many of which are randomised (operating in uncertain environments or using randomised algorithms) and timed systems (e.g. due to having to work with network transmission delays). Modelling languages and verification tools thus need to support these quantitative aspects. In this presentation, I will give an introduction to quantitative verification using the Modest modelling language and the Modest Toolset, and highlight three recent case studies with increasing demands on model expressiveness and tool capabilities: A case of power supply noise in a network-on-chip architecture modelled as a Markov chain; a case of message routing in satellite constellations that uses Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking.


All submissions will be peer-reviewed by at least three referees based on their novelty, relevance, and technical merit. The MARS proceedings will be published in the open-access EPTCS series (Electronic Proceedings in Theoretical Computer Science).

Submissions must be unpublished and not be submitted for publication elsewhere. It is accepted, however, to submit a paper about a case study already mentioned at another conference, workshop, or journal provided that: (1) the formal model is submitted to MARS 2022 and has not been published previously, and (2) the MARS submission adds significant, novel material concerning the formal modelling work.

Submissions must be in English and submitted in PDF format via EasyChair. Contributions are limited to 12 pages EPTCS style (not counting references and the appendices). Appendices (of arbitrary length, included in the proceedings) can be added to present all details of a formal model.

We welcome submissions that come together with one or many formal models that can be processed by some tool (e.g., timed automata for Uppaal, definitions and proofs for Isabelle/HOL, etc.). Such models should be complete (i.e., self-contained) and made available under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License. The models associated to accepted papers will be made available in the MARS Repository. A URL to the formal models should be provided along with the submission.

Important Dates (AoE)

Submission: Monday, 10 January 2022 Monday, 24 January 2022
Notification: Monday, 14 February 2022 Saturday, 19 February 2022
Final version: Monday, 28 February 2022
Workshop: Saturday and Sunday, 2-3 April 2022 Saturday, 2 April 2022 (as part of ETAPS 2022)

Call for Papers

As mentioned above, we invite papers that present full models of real systems, which may lay the basis for future formal analysis. The full CFP can be found here.

Program Committee

Venue and Travel Information

MARS 2022 is part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2022). Information about venue and travelling in/to Munich can be found at the webpage of ETAPS. As the main conference, the workshop is planned as an on-site event but with some degree of support for online attendance.

Workshop Organisers and Contact

All questions about the workshop should be emailed to the PC chairs Clemens Dubslaff and Bas Luttik at


MARS 2022 benefited from the financial support by the Cluster of Excellence for "Tactile Internet with Human-in-the-loop" (CeTI)
CeTI logo