最近有消息爆出 已提议将其纳入 的内核 Linux 5.20 （或者分支编号可能是 6.0，这完全取决于 Linus Torvalds 的决定，因为他对 Kernel 5.19 版本发表的评论）。
提出的建议是关于 一组实现 RV 机制的补丁 （运行时验证），这是一种在高度可靠的系统中验证正确操作的方法，以保证没有故障。
验证 通过将处理程序附加到跟踪点在运行时完成 根据自动机的预定义确定性参考模型检查执行的实际进度，该模型确定系统的预期行为。
Linux 开发人员， Daniel Bristot de Oliveira 提到：
在过去的几年里，我一直在探索使用运行时验证来验证 Linux 内核行为的可能性。
运行时验证 (RV) 是一种轻量级（但严格）的方法，它补充了经典的详尽验证技术（例如模型检查和定理证明），并以更实际的方法处理复杂系统。 VR 不依赖于系统的详细模型（例如，指令级的重新实现），而是通过分析系统的实际执行轨迹，将其与系统行为的正式规范进行比较来工作。
在 VR 中使用确定性自动机是一种行之有效的方法。 在 Linux 内核的具体案例中，您可以通过本文了解如何对 Linux 内核的复杂行为进行建模：
德奥利维拉，丹尼尔布里斯托； 库奇诺塔，托马索； 德奥利维拉，罗慕洛席尔瓦。 *Linux 内核的有效形式验证。* 在：国际软件工程和形式方法会议中。 施普林格，湛，2019 年。 315-332。
这种方法在这里的效率如何：
德奥利维拉，丹尼尔 B.； 德奥利维拉，罗慕洛 S.； 库奇诺塔，托马索。 *PREEMPT_RT Linux 内核的线程同步模型。* 系统架构杂志，2020，107：101729。
TLDR：可以以模块化方式对复杂行为进行建模，并具有可接受的开销（即使对于生产系统也是如此）。
有人提到 跟踪点信息将模型从一种状态移动到另一种状态，并且如果新状态与模型参数不匹配，则会生成警告或内核进入“恐慌”状态（假设高度可靠的系统会检测并响应此类情况）。
自动机模型 定义从一种状态到另一种状态的转换 导出为“点”格式 (graphviz)，然后使用 dot2c 实用程序将其转换为 C 表示形式，该表示形式以跟踪偏差的内核模块的形式加载。 从预定义的模型执行。
在运行时检查模型被定位为更轻更容易的方法 实施以验证关键任务系统中执行的正确性，它补充了经典的可靠性验证方法，例如模型验证和代码符合以形式语言给出的规范的数学证明。
跟踪子系统维护者 Steven Rostedt 总结如下：
» 这是此拉取请求的最大变化。 引入了在安全关键系统上运行 Linux 所需的运行时验证。 它允许将确定性自动机模型插入内核以附加到跟踪点，其中有关这些跟踪点的信息会将模型从一种状态移动到另一种状态。
RV 的上述优点之一是能够提供严格的验证，而无需使用建模语言单独实现整个系统，以及对不可预见事件的灵活响应，例如阻止关键系统故障的传播。
最后，如果您有兴趣能够了解更多，可以在 以下链接。
数据来源： https://www.phoronix.com/