RT-proofs: Formal proofs for real-time systems

• Applicants: Björn Brandenburg, Ph.D.; Professor Dr.-Ing. Rolf Ernst
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems ; Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: from 2017 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 391919384

Real-time systems, i.e., computer systems subject to stringent timing constraints, are at the heart of most modern safety-critical technologies, including automotive systems, avionics, robotics, and factory automation, to name just a few prominent domains in which incorrect timing can have potentially catastrophic consequences. To assure the always-correct operation of such systems, i.e., to make sure that they always react in a timely fashion even in a worst-case scenario, rigorous validation efforts are required prior to deployment. However, establishing that all timing constraints are met is far from trivial --- and requires sophisticated analysis techniques --- because software timing varies in complex and difficult to predict ways, e.g., due to scheduling delays, shared resources, or communication, even when executing on a dedicated processor. Unfortunately, the theoretical foundations of current analysis methods are not nearly as rock-solid as one might expect.The key problem is that the state-of-the-art methods are backed by only informal or abbreviated proofs, which are typically difficult to understand, check, adapt, or reuse. As a result, there is a non-trivial risk of subtle, but fatal mistakes, either lingering in the published literature, or arising when combining results with unstated, inconsistent assumptions. And indeed, this is not just a hypothetical concern - most famously, the timing analysis of the CAN real-time bus (widely deployed in virtually all modern cars) was refuted in 2007, 13 years after initial publication. Similarly, other lesser-known examples of incorrect worst-case analyses abound in the literature, including off-by-one errors, incorrect generalizations, and even claims that are simply wrong. Worse, even if the underlying theory is indeed flawless, there is still no guarantee that it is actually implemented correctly in the toolchains used in practice. In short, the state of the art in the analysis of safety-critical real-time systems leaves a lot to be desired - informal "pen and paper" proofs are simply inadequate.There is a better way: timing analysis results should be formally proved, machine-checkable, and independently verifiable. To this end, the RT-proofs project will lay the foundations for the computer-assisted verification of schedulability analysis results by (i) formalizing foundational real-time concepts using the Coq proof assistant and (ii) mechanizing proofs of busy-window-based end-to-end latency analysis, the analysis approach of greatest practical relevance (e.g., used by SymTA/S). Additionally, we will (iii) demonstrate with a practical prototype how trust in a vendor's toolchain can be established by certifying the produced analysis results (rather than the tool itself). Leading by example, RT-proofs will fundamentally raise the level of rigor, to the benefit of the academic community, tool vendors, and real-time systems engineers in practice.

• DFG Programme: Research Grants
• International Connection: France
• Cooperation Partners: Professor Dr. Jean-François Monin; Sophie Quinton, Ph.D.; Dr. Pierre Roux