Published: 21st March 2022
DOI: 10.4204/EPTCS.355
ISSN: 2075-2180

EPTCS 355

Proceedings Fifth Workshop on
Models for Formal Analysis of Real Systems
Munich, Germany, 2nd April 2022

Edited by: Clemens Dubslaff and Bas Luttik

Preface
Invited Presentation: An Overview of Modest Models and Tools for Real Stochastic Timed Systems
Arnd Hartmanns
1
Advanced Models for the OSPF Routing Protocol
Courtney Darville, Peter Höfner, Franc Ivankovic and Adam Pam
13
Stateful to Stateless: Modelling Stateless Ethereum
Sandra Johnson, David Hyland-Wood, Anders L Madsen and Kerrie Mengersen
27
Modeling R^3 Needle Steering in Uppaal
Sascha Lehmann, Antje Rogalla, Maximilian Neidhardt, Anton Reinecke, Alexander Schlaefer and Sibylle Schupp
40
Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
Lina Marsso, Radu Mateescu, Lucie Muller and Wendelin Serwe
60
Formal Modeling and Initial Analysis of the 4SECURail Case Study
Franco Mazzanti and Dimitri Belli
118

Preface

This volume contains the proceedings of MARS 2022, the fifth workshop on Models for Formal Analysis of Real Systems. MARS 2022 was held on the 2nd of April in Munich (Germany) as part of ETAPS 2022, the European Joint Conferences on Theory and Practice of Software. The aim of the MARS workshops is to bring together communities developing complex formal models of real systems in areas such as networks, cyber-physical systems, hardware/software codesign, biology, etc.

The motivation for organizing the MARS workshop series stems from the following two observations:

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

The formal models of real systems presented at MARS 2022 lay the basis for future analysis and comparison. In addition to the workshop proceedings, these formal models are archived in the MARS Repository. 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. Interestingly, MARS 2022 featured two contributions discussing significant enhancements of models published in MARS 2020.

Since the presentations of MARS 2020 contributions had to be canceled due to the COVID-19 pandemic, all authors of MARS 2020 contributions were invited to give a presentation at MARS 2022.

The program committee consisted of:

Clemens Dubslaff (TU Dresden, Germany, co-chair)
Hubert Garavel (INRIA Grenoble Rhône-Alpes, France)
Peter Höfner (ANU, Canberra, Australia)
Bas Luttik (TU Eindhoven, The Netherlands, co-chair)
Lina Marsso (University of Toronto, Canada)
Stefan Mitsch (Carnegie Mellon University, United States)
Thomas Neele (TU Eindhoven, The Netherlands)
Dave Parker (University of Birmingham, UK)
Martina Seidl (Johannes Kepler University Linz, Austria)
Tayssir Touili (LIPN, CNRS & University Paris 13, France)

We thank the authors who submitted papers and models to the workshop for their contributions. We thank the members of the program committee and reviewers for carefully reviewing the submissions. We are also most grateful to our guest speakers for accepting our invitation: Hugues Evrard (Google, London, UK) presented his model of the Raft Distributed Consensus Protocol in LNT, and Arnd Hartmanns (University of Twente, The Netherlands) gave an introduction to the Modest modeling language and toolset, highlighting three recent case studies.

Clemens Dubslaff and Bas Luttik