为了包含在 Linux 5.20 内核中（也许分支编号为 6.0），已经提出了一组补丁，其中实现了 RV（运行时验证）机制，这是一种检查高可靠系统上正确操作的方法保证不出现故障。 验证是在运行时通过将处理程序附加到跟踪点来完成的，跟踪点根据确定系统预期行为的自动机的预定参考确定性模型检查实际执行进度。
来自跟踪点的信息将模型从一种状态移动到另一种状态，如果新状态与模型的参数不匹配，则会生成警告或将内核置于“恐慌”状态（据了解，高可靠系统将检测此类情况并做出响应）。 定义从一种状态到另一种状态的转换的自动机模型被导出为“dot”（graphviz）格式，之后使用 dot2c 实用程序将其转换为 C 表示形式，该表示形式以跟踪偏差的内核模块的形式加载预定义模型的执行进度。
运行时模型检查被定位为一种更轻量级且易于实现的方法，用于验证关键任务系统上执行的正确性，补充了可靠性验证的经典方法，例如模型检查和代码符合给定规范的数学证明用正式语言。 RV 的优点之一是能够提供严格的验证，而无需使用建模语言单独实现整个系统，并且能够灵活响应不可预见的事件，例如阻止关键系统中故障的进一步传播。
来源： opennet.ru