Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

RT-proofs: Formale Beweise für Echtzeitsysteme

Fachliche Zuordnung Rechnerarchitektur, eingebettete und massiv parallele Systeme
Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
Förderung Förderung von 2017 bis 2022
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 391919384
 
Erstellungsjahr 2022

Zusammenfassung der Projektergebnisse

Current analysis techniques for critical real-time systems are based on complex pen-and-paper proofs that are error prone and hard to reuse. Real-time systems are at the heart of most modern safetycritical technologies, including avionics, automotive, robotics, and factory automation. To make sure they react in a timely fashion even in worst-case scenarios, rigorous validation efforts based on sophisticated timing analysis techniques are required. However, current analysis methods are backed by informal proofs, which are often difficult to follow, check, or reuse, and hence at risk of subtle, but fatal mistakes. As a result, an alarming number of unsound results had to be corrected in recent years. Famously, the timing analysis of the CAN bus (used in most modern cars) was refuted 13 years after initial publication. More recently, a systematic evaluation of the literature on self-suspending real-time systems found a large number of flaws, many of them due to an unsound generalization of a proof. Computer-assisted proofs have the potential to prevent such mathematical errors. Formalizing existing real-time analysis methods could both avoid errors in their proofs and ease their reuse, adaptation to a new context or even their combination to provide improved, more precise, results. Interactive theorem provers enable computers to automatically check mathematical proofs, ensuring they are free of reasoning errors. Proof assistants are software tools providing a formal language to express mathematical definitions, theorem statements and their proofs. The tool is then able to check the wellformedness of the definitions and statements and the validity of the proofs. Moreover, proof assistants help users interactively develop the proofs. Using a proof assistant to formalize the foundations of real-time analyses allows us to achieve the required level of confidence. At the same time, it alleviates peer review of future results, as only specifications must be agreed upon while proofs can be trusted. The past decade has shown that proof assistants have now reached a level of maturity that makes them suitable for such a task. The Coq proof assistant was chosen as it is a mature tool of which project partners had some extensive and positive prior experience. Furthermore, Coq is able to perform computations, which makes it possible to manage certificates coming from other tools, achieving a high assurance level while retaining the possibility to exploit the efficiency of specialized analysis and verification tools. We have used the Coq proof assistant to formalize the foundations of two main analysis techniques, namely classical Response Time Analyses (RTA) and Network Calculus (NC). In addition, we have built mathematical links between the Compositional Performance Analysis method (CPA), RTA and NC. Finally, Coq automatic tactics have been developed to check RTA and NC certificates. A third tool has been designed to target specifically CAN bus analysis with high efficiency. These results show the feasibility of using certified proofs for the analysis of real-time systems, as well as the many benefits resulting from it beyond certified correctness. One of the project partners was granted an ERC funding to pursue investigation on this subject and two of the project’s software tools are currently being licensed. The project yielded sixteen publications in international conferences or journals with review committees such as ECRTS, RTAS, RTNS, DATE, CAV or NFM. Most of these publications were accompanied by a Coq formalization, often based on the Prosa library developed within the project. Most of this code is available under either free open source licenses or licenses enabling non commercial use. The RT-proofs project is a fundamental research project between INRIA, ONERA and VERIMAG on the French side, and the Max-Plack Institute for Software Systems and TU Braunschweig on the German side.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2025 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung