|
Published: 27th March 2024 DOI: 10.4204/EPTCS.399 ISSN: 2075-2180 |
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 (http://mars-workshop.org/repository.html) ---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
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.
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.
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.