Formal proofs for real-time systems – RT-proofs

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 allows us the achieve the
required level of confidence, and at the same time simplify the peer
review of increasingly complex, future re- sults — 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. Moreover,
early results in the real-time domain have already been achieved.

In addition, commercial tools implementing state-of-the-art real-time
analyses, such as SymTA/S, NETCAR-Analyzer or RTaW-Pegase, 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 cer- tifying tools — by
laying the groundwork for the generation, composition, and
verification of proof certificates for response-time, blocking, and
end-to-end latency bounds.

Most of the work carried out in the RT-proofs project aims at being
formally specified and proved using the Coq proof assistant as part of the Prosa library, freely available at
prosa.mpi-sws.org

Among the current results of the project, one can notice
* An understanding of the common concepts needed for formally
describing the behavior of real-time systems and usual modeling
concepts;
* Initial results connecting the models used and results produced by
Compositional Performance Analysis and Network Calculus;
* A formalization of the busy-window principle and the corresponding
abstract response-time analysis;
* CertiCAN, a tool produced using Coq for the formal certification of
CAN analysis results.

Work performed in the project is presented in multiple publications in
international peer-reviewed conferences. The complete up to date list
can be found on the project website
(https://rt-proofs.inria.fr/publications/).

Real-time systems are at the heart of most modern safety-critical
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 lack rigor: they are backed only by
informal proofs, which are 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. Most
famously, the timing analysis of the CAN bus (used in most modern
cars) was refuted 13 years after initial publication.

Using the Coq proof assistant, the RT-proofs project will lay the
foundation for computer-assisted verification of timing analysis
results. Leading by example, RT-proofs will fundamentally raise the
level of rigor, to the benefit of both the academic community and tool
vendors.