Published: 26th April 2020
DOI: 10.4204/EPTCS.316
ISSN: 2075-2180

EPTCS 316

Proceedings of the 4th Workshop on
Models for Formal Analysis of Real Systems
Dublin, Ireland, April 26, 2020

Edited by: Ansgar Fehnker and Hubert Garavel

Preface
Invited Paper: Various Ways to Quantify BDMPs
Marc Bouissou, Shahid Khan, Joost-Pieter Katoen and Pavel Krcal
1
Invited Paper: Modeling the Raft Distributed Consensus Protocol in LNT
Hugues Evrard
15
Formalising the Optimised Link State Routing Protocol
Ryan Barry, Rob van Glabbeek and Peter Höfner
40
Formal Models of the OSPF Routing Protocol
Jack Drury, Peter Höfner and Weiyou Wang
72
Iterative Variable Reordering: Taming Huge System Families
Clemens Dubslaff, Andrey Morozov, Christel Baier and Klaus Janschek
121
Estimating End-to-End Latencies in Automotive Cyber-physical Systems
Max J. Friese and Dirk Nowotka
134
Specifying a Cryptographical Protocol in Lustre and SCADE
Lina Marsso
149
Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour and Marc Renaudin
200
Simulation-based Safety Assessment of High-level Reliability Models
Simon József Nagy, Bence Graics, Kristóf Marussy and András Vörös
240
Synthesizing Strategies for Needle Steering in Gelatin Phantoms
Antje Rogalla, Sascha Lehmann, Maximilian Neidhardt, Johanna Sprenger, Marcel Bengs, Alexander Schlaefer and Sibylle Schupp
261

Preface

This volume contains the proceedings of MARS 2020, the fourth workshop on Models for Formal Analysis of Real Systems, held as part of ETAPS 2020, the European Joint Conferences on Theory and Practice of Software.

The MARS workshop brings 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 MARS workshops stem from two observations:

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

The formal models of real systems presented at MARS 2020 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.

We would like to thank the program committee members:

Christel Baier (TU Dresden) Dimitra Giannakopoulou (NASA Ames)
Jan Friso Groote (TU Eindhoven) Holger Hermanns (Saarland University)
Peter Höfner (Data61) Rob van Glabbeek (Data61)
Kim Larsen (Aalborg University) Dave Parker (University of Birmingham)
Natasha Sharygina (USI Lugano, Switzerland) Tayssir Touili (LIPN, CNRS & University Paris 13)

We are also grateful to the following reviewers for their participation in the evaluation process:

Nicolas Amat Elvio Amparore Sepideh Asadi Timothy Bourke
Pierre Bouvier Mark Bouwman Carlos Budde Franck Cassez
Bert de Brock Marcus Gerhold Nicolas Halbwachs Michaela Klauck
Frédéric Lang Matteo Marescotti Rodrigo Otoni Vivien Quema
Arash Khabbaz Saberi

Each paper received at least four reviews, and the reviews also included an evaluation of the submitted models. The review process was characterised by lively and sometimes spirited discussions, which underlines the commitment of the community, the relevance of the workshop, and the importance of formal models as a primary source for research.

Of course, we also thank all colleagues who took the time to write and submit papers to to the workshop. We are also most grateful to our guest speakers for accepting our invitation: Hugues Evrard (Google, London, UK) who presents his model of the Raft Distributed Consensus Protocol in LNT, and Marc Bouissou (Electricité de France R&D, France) who will present various ways to quantify Boolean-logic-driven Markov processes, a joint work with Shahid Khan and Joost-Pieter Katoen (RWTH Aachen, Germany), and Pavel Krcal (RiskSpectrum, Lloyd's Register, Sweden).

Acknowledgement are due to INRIA Grenoble for providing financial support to MARS 2020.

Ansgar Fehnker and Hubert Garavel