RT-proofs: Formal proofs for real-time systems

实时系统，即受严格时间限制的计算机系统，是大多数现代安全关键技术的核心，包括汽车系统、航空电子、机器人和工厂自动化，仅举几个突出的领域，在这些领域中，不正确的时间可能会产生潜在的灾难性后果。为确保这类系统始终正确运行，即确保它们即使在最坏的情况下也总是及时作出反应，在部署之前需要进行严格的验证工作。然而，确定满足所有定时约束绝非易事-并且需要复杂的分析技术-因为软件定时以复杂且难以预测的方式变化，例如，由于调度延迟、共享资源或通信，即使当在专用处理器上执行时也是如此。不幸的是，当前分析方法的理论基础并不像人们想象的那样坚如磐石。关键问题是，最先进的方法只有非正式或简短的证据支持，这些证据通常很难理解、检查、适应或重复使用。因此，存在着微妙但致命的错误的风险，这些错误要么在已出版的文献中挥之不去，要么在将结果与未陈述的、不一致的假设相结合时出现。事实上，这不仅仅是一个假想的问题--最著名的是，对CAN实时总线(几乎所有现代汽车都广泛使用)的时序分析在最初发布13年后的2007年被驳斥。同样，文献中还有其他不太为人所知的不正确的最坏情况分析的例子，包括一对一的错误、不正确的概括，甚至是完全错误的主张。更糟糕的是，即使潜在的理论确实是完美的，仍然不能保证它实际上在实践中使用的工具链中得到了正确的实现。简而言之，安全关键型实时系统分析的最新水平还有很多不尽如人意的地方--非正式的纸笔证明是不够的。还有一种更好的方法：定时分析结果应该得到正式证明，机器可以检查，并且可以独立验证。为此，RT-Profect项目将通过以下方式为可调度性分析结果的计算机辅助验证奠定基础：(I)使用CoQ证明助手将基本的实时概念形式化，以及(Ii)基于忙窗口的端到端延迟分析的机械化证明，这是最具实际相关性的分析方法(例如，SYNTA/S使用的方法)。此外，我们将(Iii)用一个实际的原型演示如何通过认证产生的分析结果(而不是工具本身)来建立对供应商工具链的信任。以身作则，RT证明将从根本上提高严格性水平，使学术界、工具供应商和实践中的实时系统工程师受益。

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.