包括Lustre mannul , Lustre internals , Lustre quick start ,Lustre arthitecture等资料
2024-03-29 16:21:20
13.84MB
1
种类2
是基于Lustre程序安全性的多引擎，基于SMT的并行并行自动模型检查器。
种类2是命令行工具。 它以注有被证明为不变的属性的Lustre文件作为输入（请参见 ），并输出所有输入中正确的属性，以及伪造的那些属性的输入序列。 为了简化外部工具的处理，种类2可以将结果以JSON和XML格式 （请参阅 ）。
默认情况下，种类2运行用于边界模型检查（BMC）的过程，用于k归纳的两个过程（一个用于k = 2的固定值，另一个用于增加k的值），几个用于不变生成的过程以及一个过程同时对所有属性的IC3进行并行处理。 它以增量方式将反例输出到属性以及经证明是不变的属性。
以下命令行选项控制其操作（运行kind2 --help可获得完整列表）。 见用于配置实例和每种技术的更多细节。
--enable {BMC|IND|IND2|IC3|INVGEN|INVGENOS|...}选择模型检查引擎
2021-12-16 21:05:34
2.1MB
1