Specification and Verification for MIMOS, our Framework for design and Update of Real-Time Embedded Systems
Traditionally, critical software in embedded real-time systems is statically verified, and once certified supposed to remain valid for the lifetime of the system itself. Modern systems, evolving in more and more open and evolving contexts impose new requirements on embedded software. MIMOS proposes a paradigm shift to respond to these challenges by means of a combination of features: (1) it is high-level and strictly model-based concerning functional and non-functional aspects to guarantee intuitive concepts to the designer whose semantics is preserved. (2) It proposes a framework for static and dynamic (monitoring-based) verification of functionality and timing completing each other. (3) Finally, our ultimate goal is allowing to ease update of critical software.
The talk will give an overview on the MIMOS concepts and the tool environment for embedded and real-time systems design developed in Uppsala within Wang Yi's ERC CUSTOMER project. Particular focus will be on the specification and verification framework that we are developing in this context.
Susanne Graf
is a research professor (Directeur de Recherche CNRS) at VERIMAG of Grenoble University. She has a PhD in Computer Science from Polytechnical Institute of Grenoble. Her Research interest has always been focused on formal approaches to design and verification in different application domains. Today her main interest is design and analysis of embedded real-time systems. In 2022 she received the CAV award for her pioneering work on predicate abstraction.
Design Principles for Reducing the Complexity of Safety-Critical Embedded Systems
System Architecting deals with the decomposition of a large complex system into almost independent parts in order to reduce the implementation and validation efforts by applying the time-tested design principle divide et impera. In this presentation, we present some additional proven design principles for decomposing complex safety-critical embedded systems using the control system of a fully autonomous vehicle as an example. With the current state of the art in hardware and software, it is impossible to achieve the required safety goals of such a large complex computer system by implementing a non-fault tolerant monolithic computer architecture. We need to find a decomposition into independent Fault Containment Units (FCUs) such that a Byzantine failure of any complex FCU can be mitigated by the other correct FCUs without causing a catastrophic incident. We start by the establishment of the required safety goals and propose to make a clear distinction between the two important use cases: (i) correct behavior under well-specified nominal conditions, and (ii) safe behavior under off-nominal conditions, which cannot be fully specified in advance.
Hermann Kopetz
is professor emeritus at TU Wien. He received a PhD degree in Physics sub auspiciis praesidentis from the University in Vienna in 1968. Kopetz is the chief architect of the time-triggered technology for dependable embedded Systems and a co-founder of the company TTTech. The time-triggered technology is deployed in leading aerospace, automotive and industrial applications. Kopetz is a Life Fellow of the IEEE and a full member of the Austrian Academy of Science. Kopetz served as the chairman of the IEEE Computer Society Technical Committee on Dependable Computing and Fault Tolerance and in program committees of many scientific conferences. He is a founding member and a former chairman of IFIP WG 10.4. Kopetz has written a widely used textbook on Real-Time Systems—the third edition has been published in 2022— and authored more than 400 papers. In June 2007 he received the honorary degree of Dr. honoris causa from the University Paul Sabatier in Toulouse, France.