verification - 我应该使用计算机辅助验证工具吗？

Question

我有兴趣证明一些机器人控制器没有达到任何故障状态，我将通过一组谓词来定义它。我知道有开源软件工具可以实现这一目标。例如，我听说过BLAST（Berkeley Lazy Abstraction Software Verification Tool），但您是否知道任何其他可能更易于使用和/或更针对我的特定应用程序的工具？

您是否曾经在您的一个项目中使用过 BLAST 或其他此类工具，您是否认为收益超过部署此类工具所需的努力？

Answer 1

您可能会发现Frama-C很有用。

对于非 Frama-C 开发人员的评估，请参阅这两篇文章。一些开发安全关键代码（例如 DO-178B A 级）的工程师发现，基于最弱前置条件技术的正式注释和分析值得投资，但传统测试对他们来说非常昂贵。最后一个链接是关于 Caveat 的，这是一个 Frama-C 打算在适当时候替换的闭源分析器。

您的问题听起来好像您可能会欣赏 Frama-C 的Aoraï插件。

在你的情况下，这是否所有的时间都值得花更多的时间可能更多的是你是否认为学习这些技术是一种乐趣或苦差事。