6th Workshop on
Models for Formal Analysis of Real Systems
(MARS 2024)

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.

8:50-9:00	Opening
9:00-10:00	Invited Talk I (Chair: Hubert Garavel) Signal-based temporal properties for cyber-physical systems: specification, monitoring, and diagnostics  Domenico Bianculli
10:00-10:30	Coffee Break
10:30-12:30	Protocol modelling and comparison of models (Chair: Matthias Volk) Modelling the Raft Distributed Consensus Protocol in mCRL2  Parth Bora, Minh Pham Duc and Tim Willemse Four Formal Models of IEEE 1394 Link Layer  Hubert Garavel and Bas Luttik Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment  Kevin Jilissen, Peter Dieleman and Jan Friso Groote Testing Resource Isolation for System-on-Chip Architectures  Philippe Ledent, Radu Mateescu and Wendelin Serwe
12:30-14:00	Lunch Break
14:00-15:00	Invited Talk II (Chair: Rob van Glabbeek) Validating Traces of Distributed Programs against High-Level Specifications  Stephan Merz
15:00-16:00	Verification of controllers (Chair: Frédéric Lang) Formal Verification of Consistency for Systems with Redundant Controllers  Bjarne Johansson, Bahman Pourvatan, Zahra Moezkarimi, Alessandro Papadopoulos and Marjan Sirjani Sliced Online Model Checking for Optimizing the Beam Scheduling Problem in Robotic Radiation Therapy  Lars Beckers, Stefan Gerlach, Ole Lübke, Alexander Schlaefer and Sibylle Schupp
16:00-16:30	Coffee Break
16:30-17:30	Invited Talk III (Chair: Marjan Sirjani) Debugging Embedded Systems Requirements with STIMULUS  Bertrand Jeannet
17:30-17:40	Closing
19:00-	Informal workshop dinner, La Veranda.

Invited Talks

Signal-based temporal properties for cyber-physical systems: specification, monitoring, and diagnostics by Domenico Bianculli (University of Luxembourg, Luxembourg)
Abstract. Run-time verification (RV) is an analysis technique that focuses on observing the execution of a system to check its expected behavior against some specification. It is used for software verification and validation activities, such as operationalizing test oracles and defining run-time monitors.
The three main components of an effective RV approach are: i) a specification language allowing users to formally express the system requirements to be checked; ii) a monitoring algorithm that checks a system execution trace against the property specifications and yields a verdict indicating whether the input traces satisfies the property being checked; iii) a diagnostics algorithm that explains the cause of a requirement violation, in case of a negative verdict.
In this talk, I will review these three aspects taking into account the perspective of signal-based temporal properties for cyber-physical systems and will report on the application of the proposed formal methods in the context of collaborative research projects with industrial partners.

Validating Traces of Distributed Programs against High-Level Specifications by Stephan Merz (University of Lorraine, CNRS, Inria, LORIA, Nancy, France)
Abstract. This talk presents joint work with Horatiu Cirstea, Benjamin Loillier, and Markus Kuppe.
TLA+ is widely used for describing and verifying distributed algorithms at a high level of abstraction. We present ongoing work on validating traces of distributed programs with respect to TLA+ specifications. This work is supported by a library for instrumenting processes in order to log the values of variables of the TLA+ specification as well as informations about the execution of events. After merging the logs of individual processes, a trace of the distributed execution is obtained, and the TLA+ model checker is used to check if this trace corresponds to a prefix of an execution allowed by the TLA+ specification.
Our experience with the approach has shown that although it cannot establish the correctness of an implementation, it is very effective for detecting discrepancies between executions of the distributed program and the high-level specification. Our framework requires neither the complete state of the TLA+ specification nor all events to be represented in the trace because we rely on the model checker to resolve potential non-determinism, and we discuss tradeoffs between precision of tracing and complexity of model checking.

Debugging Embedded Systems Requirements with STIMULUS by Bertrand Jeannet, (Dassault Systèmes, France)
Abstract. STIMULUS is an application dedicated to the early debugging and validation of functional real-time systems requirements, that has been developed in the start-up Argosim and since 2019 in Dassault Systèmes, and that addresses safety-critical embedded systems (transportation, aerospace, energy, etc…). It provides a high-level language to express textual yet formal requirements, and a solver-driven simulation engine to generate and analyze execution traces that satisfy these requirements. Visualizing what systems can do enables system architects to discover ambiguous, incorrect, missing or conflicting requirements before the design begins.
We first present the scientific foundations of STIMULUS, which is based on a constraint synchronous programming language, in which the data-flow equations of Lustre and Lucid Synchrone languages are generalized to data-flow constraints relating several signals.
We then demonstrate the use of STIMULUS on the specification of automatic headlights from the automotive industry. We show how this unique simulation technique enables to discover and to fix ambiguous and conflicting requirements, resulting in a clear and executable specification that can be shared among engineers.

Workshop Dinner

An informal workshop dinner is planned at 7pm in the restaurant of Parc Hôtel Alvisse, La Veranda. The dinner is open to all participants. Please contact the PC chairs if you did not receive information.

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 2024 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.

Submission:	Monday, 15 January, 2024 Thursday, 25 January, 2024
Notification:	Saturday, 24 February, 2024 Wednesday, 28 February, 2024
Final version:	Monday, 11 March, 2024
Workshop:	Saturday, 6 April, 2024 (as part of ETAPS 2024)

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.

MARS 2024 is part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2024). Information about venue and travelling in/to Luxembourg can be found at the webpage of ETAPS.

All questions about the workshop should be emailed to the PC chairs Frédéric Lang and Matthias Volk at mars2024@mars-workshop.org