Kind2: 基于多引擎SMT的自动模型检查器，保障Lustre程序的安全性

简介：
Kind2是一款先进的自动模型检查工具，专为验证Lustre程序设计。它采用多引擎SMT技术，确保软件系统的安全性和可靠性，是开发高质量嵌入式控制软件的理想选择。 种类2是一种基于Lustre程序安全性的多引擎并行自动模型检查器，并且它使用SMT技术进行验证工作。作为一种命令行工具，种类2接受带有被证明为不变属性的Lustre文件作为输入，并输出所有正确的和错误的属性及其对应的反例序列。 为了方便外部工具处理结果，种类2支持将结果以JSON或XML格式导出。默认情况下，它会运行边界模型检查（BMC）过程、两个k归纳的过程（一个用于固定值k=2的情况，另一个则逐步增加k）、几个不变生成的过程以及针对所有属性的IC3并行处理。 在执行过程中，种类2能够以增量方式输出反例给属性及其经证明为不变的实例。可以通过命令行选项--enable {BMC|IND|IND2|IC3|INVGEN|INVGENOS...}来选择模型检查引擎，并且运行kind2 --help可以查看所有可用选项的具体列表。 更多关于配置和各种技术细节的信息，请参阅相关文档或指南。