Published: 27th March 2024
DOI: 10.4204/EPTCS.399
ISSN: 2075-2180


Proceedings Sixth Workshop on
Models for Formal Analysis of Real Systems
Luxembourg City, Luxembourg, 6th April 2024

Edited by: Frédéric Lang and Matthias Volk

Invited Presentation: Signal-Based Temporal Properties for Cyber-Physical Systems: Specification, Monitoring, and Diagnostics
Domenico Bianculli
Invited Presentation: Validating Traces of Distributed Programs against High-Level Specifications
Stephan Merz
Invited Presentation: Debugging Embedded Systems Requirements with STIMULUS
Bertrand Jeannet
Modelling the Raft Distributed Consensus Protocol in mCRL2
Parth Bora, Pham Duc Minh and Tim A.C. 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 H.J. Jilissen, Peter Dieleman and Jan Friso Groote
Testing Resource Isolation for System-on-Chip Architectures
Philippe Ledent, Radu Mateescu and Wendelin Serwe
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


This volume contains the proceedings of MARS 2024, the sixth workshop on Models for Formal Analysis of Real Systems, held on April 6, 2024 in Luxembourg City, Luxembourg, as part of ETAPS 2024, the European Joint Conferences on Theory and Practice of Software.

The MARS workshop series addresses the formal modelling of realistic systems. Making a formal model of a system is a necessary prerequisite for its formal analysis and for formal verification of its correctness.

To show the applicability of tools and techniques for verification and analysis, toy examples or tiny case studies are typically presented in research papers. Since the theory needs to be developed first, this approach is reasonable. However, to show that a developed approach actually scales to real systems, large case studies are essential. The development of formal models of real systems usually requires a perfect understanding of informal descriptions of the system ---sometimes found in RFCs or other standard documents--- which are usually just written in English. Based on the type of system, an adequate specification formalism needs to be chosen, and the informal specification needs to be translated into it. Examples for such formalisms include process and program algebra, Petri nets, variations of automata, as well as timed, stochastic and probabilistic extensions of these formalisms. Abstraction from unimportant details then yields an accurate, formal model of the real system.

The process of developing a detailed and accurate model usually takes a considerable amount of time, often months or years; without even starting a formal analysis. When publishing the results on a formal analysis in a scientific paper, details of the model usually have to be skipped due to lack of space, and often the lessons learnt from modelling are not discussed since they are not the main focus of the paper.

The MARS workshops aim at discussing exactly these unmentioned lessons. Examples are:

MARS emphasises modelling over verification. In particular, we invited papers that present full models of real systems, which may lay the basis for future comparison and analysis. The workshop thus intends to bring together researchers from different communities that all aim at verifying real systems and are developing formal models for such systems. An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them.

Full specifications of the contributed models are available online at the MARS Repository ( ---often including executable models--- so that their quality can be evaluated. Alternative formal descriptions are encouraged, which should foster the development of improved specification formalisms.

The MARS 2024 workshop included talks by three invited speakers: Domenico Bianculli (University of Luxembourg, Luxembourg) presented recent work on runtime verification of signal-based temporal properties for cyber-physical systems; Stephan Merz (University of Lorraine, CNRS, Inria, LORIA, Nancy, France) presented work on the validation of traces of distributed programs against high-level specifications; and Bertrand Jeannet (Dassault Systèmes, France) presented work on the STIMULUS tool, dedicated to the early debugging and validation of functional real-time systems requirements.

The body of this volume contains six contributions. The submitted papers were carefully refereed by at least three members of the programme committee. The topics include:

We would like to thank the program committee members:

We are also grateful to the following reviewers:

We wish to express our gratitude to the authors who submitted papers, the speakers, and the invited speakers. Thanks are also due to the EasyChair organisation for supporting the various tasks related to the selection of the contributions and also EPTCS and arXiv for publishing and hosting the proceedings.

Frédéric Lang and Matthias Volk

Signal-Based Temporal Properties for Cyber-Physical Systems: Specification, Monitoring, and Diagnostics

Domenico Bianculli (University of Luxembourg)

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

Stephan Merz (University of Lorraine, CNRS, Inria, LORIA, Nancy, France)

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

Bertrand Jeannet (Dassault Systèmes)

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.