-
A formal specification of the desired software behaviour of the Princess Marijke lock complex
Authors:
Jan Friso Groote,
Matthias Volk
Abstract:
The Princess Marijke lock complex is a large lock and water-protection installation in the Netherlands between the river Rhine and the Amsterdam-Rijnkanaal -- a large waterway connecting the Rhine to the port of Amsterdam. The lock complex consists of two independent locks and a moveable flood-protection barrier. Ensuring safe control of the lock complex is of utmost importance to guarantee both f…
▽ More
The Princess Marijke lock complex is a large lock and water-protection installation in the Netherlands between the river Rhine and the Amsterdam-Rijnkanaal -- a large waterway connecting the Rhine to the port of Amsterdam. The lock complex consists of two independent locks and a moveable flood-protection barrier. Ensuring safe control of the lock complex is of utmost importance to guarantee both flood-protection and reliable ship operations. This paper gives a precise, formal description of the software control of the lock complex in less than 400 lines of mCRL2 code. This description can act as a blueprint on how the software of this lock complex needs to be constructed. Moreover, using model checking, 53 software requirements are shown to be valid, ensuring that the formal description of the behaviour is correct with regard to these properties and is unlikely to contain mistakes and oversights.
△ Less
Submitted 3 July, 2025;
originally announced July 2025.
-
A Formally Verified Fail-Operational Safety Concept for Automated Driving
Authors:
Yuting Fu,
Andrei Terechko,
Jan Friso Groote,
Arash Khabbaz Saberi
Abstract:
Modern Automated Driving (AD) systems rely on safety measures to handle faults and to bring vehicle to a safe state. To eradicate lethal road accidents, car manufacturers are constantly introducing new perception as well as control systems. Contemporary automotive design and safety engineering best practices are suitable for analyzing system components in isolation, whereas today's highly complex…
▽ More
Modern Automated Driving (AD) systems rely on safety measures to handle faults and to bring vehicle to a safe state. To eradicate lethal road accidents, car manufacturers are constantly introducing new perception as well as control systems. Contemporary automotive design and safety engineering best practices are suitable for analyzing system components in isolation, whereas today's highly complex and interdependent AD systems require novel approach to ensure resilience to multi-point failures. We present a holistic safety concept unifying advanced safety measures for handling multiple-point faults. Our proposed approach enables designers to focus on more pressing issues such as handling fault-free hazardous behavior associated with system performance limitations. To verify our approach, we developed an executable model of the safety concept in the formal specification language mCRL2. The model behavior is governed by a four-mode degradation policy controlling distributed processors, redundant communication networks, and virtual machines. To keep the vehicle as safe as possible our degradation policy can reduce driving comfort or AD system's availability using additional low-cost driving channels. We formalized five safety requirements in the modal mu-calculus and proved them against our mCRL2 model, which is intractable to accomplish exhaustively using traditional road tests or simulation techniques. In conclusion, our formally proven safety concept defines a holistic design pattern for designing AD systems.
△ Less
Submitted 11 November, 2020; v1 submitted 2 November, 2020;
originally announced November 2020.
-
Proceedings Workshop on Models for Formal Analysis of Real Systems
Authors:
Rob van Glabbeek,
Jan Friso Groote,
Peter Höfner
Abstract:
This volume contains the proceedings of MARS 2015, the first workshop on Models for Formal Analysis of Real Systems, held on November 23, 2015 in Suva, Fiji, as an affiliated workshop of LPAR 2015, the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning.
The workshop emphasises modelling over verification. It aims at discussing the lessons learned from m…
▽ More
This volume contains the proceedings of MARS 2015, the first workshop on Models for Formal Analysis of Real Systems, held on November 23, 2015 in Suva, Fiji, as an affiliated workshop of LPAR 2015, the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning.
The workshop emphasises modelling over verification. It aims at discussing the lessons learned from making formal methods for the verification and analysis of realistic systems. Examples are:
(1) Which formalism is chosen, and why?
(2) Which abstractions have to be made and why?
(3) How are important characteristics of the system modelled?
(4) Were there any complications while modelling the system?
(5) Which measures were taken to guarantee the accuracy of the model?
We invited papers that present full models of real systems, which may lay the basis for future comparison and analysis. An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them. Alternative formal descriptions of the systems presented at this workshop are encouraged, which should foster the development of improved specification formalisms.
△ Less
Submitted 8 November, 2015;
originally announced November 2015.
