Published: 26th April 2020|
|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|
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