Aim
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 MARS workshops stem from 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.
Programme: List of Accepted and Invited Talks
- Invited talk: Various Ways to Quantify
BDMPs
Marc Bouissou (Electricité de France R&D, France)
joint work with Shahid Khan and Joost-Pieter Katoen (RWTH Aachen, Germany)
and Pavel Krcal (RiskSpectrum, Lloyd's Register, Sweden) - Invited talk: Modeling the Raft Distributed
Consensus Protocol in LNT
Hugues Evrard (Google, London, UK) -
Formalising the Optimised Link State Routing
Protocol
Ryan Barry, Rob van Glabbeek, and Peter Höfner -
Formal Models of the OSPF Routing Protocol
Jack Drury, Peter Höfner, and Weiyou Wang -
Iterative Variable Reordering: Taming Huge System
Families
Clemens Dubslaff, Andrey Morozov, Christel Baier, and Klaus Janschek -
Estimating End-to-End Latencies in Automotive
Cyber-physical Systems
Max J. Friese and Dirk Nowotka -
Specifying a Cryptographical Protocol in Lustre and SCADE
Lina Marsso -
Modeling an Asynchronous Circuit Dedicated to the
Protection Against Physical Attacks
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, and Marc Renaudin -
Simulation-based Safety Assessment of High-level
Reliability Models
András Vörös, Bence Graics, Kristóf Marussy and Simon József Nagy -
Synthesizing Strategies for Needle Steering in
Gelatin Phantoms
Antje Rogalla, Sascha Lehmann, Maximilian Neidhardt, Johanna Sprenger, Marcel Bengs, Alexander Schlaefer, and Sibylle Schupp
Submission
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 2020 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. Formal models should be put in a TAR or ZIP file, and sent by email to mars2020@mars-workshop.org, mentioning the number assigned by Easychair to the corresponding submitted paper.
Important Dates (AoE)
| Submission: | Extended to Monday, January 20, 2020 | |
| Notification: | Sunday, February 23, 2020 | |
| Final version: | Sunday, March 15, 2020 | |
| Proceedings published: | Sunday, April 26, 2020 | |
| Workshop: | Fall 2020, as part of ETAPS 2020 |
Call for Papers
Program Committee
- Christel Baier (TU Dresden, Germany)
- Ansgar Fehnker (University of Twente, The Netherlands, co-chair)
- Hubert Garavel (INRIA Grenoble Rhône-Alpes, France, co-chair)
- Dimitra Giannakopoulou (NASA Ames, California, USA)
- Jan Friso Groote (Eindhoven University of Technology, The Netherlands)
- Holger Hermanns (Saarland University, Germany)
- Peter Höfner (Data61, CSIRO, Australia)
- Rob van Glabbeek (Data61, CSIRO, Australia)
- Kim Larsen (Aalborg University, Denmark)
- Dave Parker (University of Birmingham, UK)
- Natasha Sharygina (USI Lugano, Switzerland)
- Tayssir Touili (LIPN, CNRS & University Paris 13, France)
Venue and Travel Information
MARS 2020 is part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2020). Information about venue and travelling in/to Dublin can be found at the webpage of ETAPS.
Workshop Organisers and Contact
All questions about the workshop should be emailed to Ansgar Fehnker and Hubert Garavel at mars2020@mars-workshop.org
Support
MARS 2020 benefited from the financial support of
