Machine-check：数字系统的形式化验证工具

Machine-check 是一个用于数字系统属性形式化验证的工具，目前处于实验阶段。

与经典的软件测试不同，软件测试可以发现错误但无法证明其不存在，形式化验证可以证明指定的不良行为永远不会在系统中发生。遗憾的是，形式化验证需要复杂的推理（例如，使用区间而不是仅使用数字）和先进的自动化技术。 Machine-check 旨在提供这些技术，但尽可能地将它们屏蔽起来。

machine-check 的主要预期用途是简单微控制器上的机器码程序的形式化验证，但该方法高度通用，只要它们是用 machine-check 能理解的有效 Rust 代码子集描述的任意数字系统，就可以进行验证。

示例

一个可以用 machine-check 验证的非常简单的系统示例是 counter，这是一个简单的 有限状态机，它包含一个八位的 value，初始化为零，然后在 increment 单比特输入为 1 时增加。如果值达到 157，则立即重新置为零。该系统非常简单，因此通过一个大型的未使用位向量数组稍微复杂化，这将使简单的自动化验证变得不可能。

machine-check 的魔力是通过 machine_description 宏释放的，该宏将其应用于代码的验证类似项，允许简单地通过在构建系统后在主函数中调用 [run] 来运行 machine-check。

如果您将 counter 放入您自己的 Rust 包（将 machine-check 作为依赖项），您可以使用基于 计算树逻辑 的规范属性验证计数器在每个系统状态中始终小于 157。让我们用 machine-check 证明这个属性

$ cargo run -- --property "AG[unsigned_lt(value,157)]"

[2024-03-07T22:44:44Z INFO  machine_check_exec] Starting verification.
[2024-03-07T22:44:44Z INFO  machine_check_exec] Verification ended.
{"result":{"Ok":true},"stats":{"num_states":178,"num_refinements":309}}

(请注意，最终的规范和输出格式仍在建设中，将比这更好。）

另一方面，机器检查告诉我们，计数器的值并不总是小于156。

$ cargo run -- --property "AG[unsigned_lt(value,156)]"

$ cargo run -- --property "AG[unsigned_lt(value,156)]"
[2024-03-07T22:45:47Z INFO  machine_check_exec] Starting verification.
[2024-03-07T22:45:47Z INFO  machine_check_exec] Verification ended.
{"result":{"Ok":false},"stats":{"num_states":178,"num_refinements":308}}

您可以使用“-v”命令行参数来显示最终的抽象状态空间，尽管解读它需要一些额外的知识。

固有恐慌

检测系统恐慌也是可能的，这对于例如从命令行获取机器代码文件的机器代码系统很有用，这些系统应在程序执行过程中检测是否有保留指令可以执行。一个简单的例子是在conditional_panic示例中，如果输入等于1，它应该会引发恐慌，信息为“示例恐慌2”。您可以将它复制到您的crate中，然后使用参数“--inherent”运行它，这表示您只对系统的固有恐慌感兴趣

$ cargo run -- --inherent
[2024-03-07T22:59:26Z INFO  machine_check_exec] Starting verification.
[2024-03-07T22:59:26Z ERROR machine_check_exec] Verification failed.
{"result":{"Err":{"InherentPanic":"Example panic 2"}},"stats":{"num_states":3,"num_refinements":8}}

目前，固有恐慌的存在阻止了对属性的验证，因为修复它是一个更为紧迫的问题。

机器代码验证

在simple_risc中也有一个极其简化的RISC微控制器的示例，展示了可以用来优雅地转录基于指令操作码的微控制器行为的bitmask_switch宏。

在crate machine-check-avr中，有对实际微控制器的一个更合适的实现，允许验证AVR ATmega328P微控制器（尤其是在Arduino Uno R3中使用）的一些简单机器代码程序。

当前状态

机器检查仍处于实验阶段，用户体验和验证能力有限。

特别是，machine_description宏目前非常挑剔，产生的错误可能有用也可能没用。如果您想尝试编写自己的系统，请逐步进行，缓慢地添加和修改示例代码的一部分。暂时注释掉宏也可能揭示底层的Rust错误，并带有更合理的错误信息。

其他说明

与一些其他形式化验证工具不同，机器检查旨在保证正确无误。您应该要么得到错误，要么在有限（但实际上是无界的）时间内得到正确/错误的正确结果。当然，可能会有错误或设计上的疏忽。

许可证

根据您的选择，许可为Apache许可证2.0版或MIT许可证。除非您明确声明，否则根据Apache-2.0许可证定义的，您有意提交以包含在此crate中的任何贡献，将按上述方式双重许可，不附加任何额外条款或条件。