Real-time systems are systems that must satisfy timing requirements. These systems are everywhere in our lives, ranging from cars to airplanes to mobile phones. Establishing real-time properties, such as bounds on the maximum time that a system requires to respond to a given stimulus, is a nontrivial challenge because tasks executing on the same or different processors may have complex timing influences on each other due to e.g. scheduling, shared resources, precedence constraints, or communication-related interference.
There exists by now a large body of research on real-time systems analysis methods. However, the underlying proofs for all these analyses are too often somewhat informal or difficult to check. Worse, even if the underlying theory is actually flawless, there is still no guarantee that it is actually implemented correctly in the toolchains used in practice. In short, using pen and paper proofs for the analysis of safety-critical real-time systems is simply inadequate.
To ensure the continued viability and practical relevance of real-time systems analysis in the certification of safety-critical systems, a strong, trustworthy formal basis is needed. Using a proof assistant such as Coq to formalize these foundations will allow us the achieve the required level of confidence, and at the same time simplify the peer review of increasingly complex, 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 large systems.
In addition, commercial tools implementing state-of-the-art real-time analyses cannot guarantee correctness of the results that they compute. This is partly due to the lack of formal support for the analysis itself, but also results from the effort that would be needed to certify such complex tools. Given that certification and safety assurance requirements are constantly evolving (in particular in the automotive sector, a key sector for real-time tool vendors, with the advent of the ISO26262 standard), this certification gap is posed to become a major bottleneck with substantial practical implications in the embedded industry. To tackle this challenge, the RT- PROOFS project aims to certify analysis results — in contrast to certifying tools — by laying the groundwork for the generation, composition, and verification of proof certificates for response-time, blocking, and end-to-end latency bounds.
