[巴黎高师课程] 同步反应式系统(2024-2025)第三课 - Kind 2: 基于SMT的Lustre模型检查器

在2024-2025学期的巴黎高师同步反应式系统(2024-2025)第三课中，详细讨论了基于SMT的Lustre模型检查器Kind 2的工作。本文将提供对Kind 2的介绍。对课程的详细内容，可参考同步反应式系统

简介

本节课讨论了基于SMT（Satisfiability Modulo Theories）的转换系统模型检验技术，涵盖从基本概念到具体应用的多个方面。课程中讨论了两种性质：安全性和活性性质，并解释了它们在系统验证中的重要性。接着详细介绍了SMT求解器的基础知识，包括SAT求解器的发展历程及其与SMT求解器的关系。随后讨论了模型检验的不同方法，如显式状态枚举、基于BDD的算法、有界模型检验和k-归纳法等。特别地，文章深入探讨了k-归纳法的具体实现和优化策略，包括路径压缩和抽象化技术。最后，介绍了用于Lustre程序的SMT模型检验工具Kind 2，展示了如何利用SMT技术进行形式化验证。

Kind 2 介绍

Kind 2是一款基于SMT的开源多引擎自动模型检查器，用于验证以Lustre语言扩展形式表达的有限状态或无限状态同步反应系统的安全性属性。在基础配置中，该工具接收一个或多个标注了待证明不变属性的Lustre文件作为输入，并为每个属性输出确认结果或反例（即违反该属性的输入序列）。其高级功能包括基于合约的组合验证、已证明属性的证书生成，以及基于合约的测试用例生成。

核心功能

支持Lustre V4及部分V6语法特性：

• C风格机器整数的有符号/无符号版本
• If-Then-Else条件块与Frame Condition块
• 精化类型系统
• 基于假设/保证的合约语言
• 模块化组合验证
• 反例与证据生成
• 证明证书生成
• 通过以下计算进行优劣归因分析：

归纳有效性核心(Inductive Validity Cores)

最小割集(Minimal Cut Sets)

• 合约可实现性与可满足性检查
• 针对不可实现合约的死锁轨迹生成
• 非空虚性检查：

条件属性

合约模式蕴含关系

• 合约假设生成

多模型检查引擎支持：

• 有界模型检查(BMC)
• 带惰性路径压缩的k归纳法
• IC3/PDR算法
• 基于模板的系统语法分析及不变式发现
• 基于消息传递的模型检查引擎并行组合
• 基于图的不变式生成
• 引擎间共享已发现不变式

后端推理引擎支持多种SMT求解器：
Bitwuzla、cvc5、MathSAT5、SMTInterpol、Yices 2、Yices 1及Z3

附加功能：

• 将可执行Lustre模型编译为Rust代码
• 测试用例生成

参考

• Kind 2: kind2-mc.github.io/kind2/
• 课程课件: 同步反应式系统第三课 - Kind 2: 基于SMT的Lustre模型检查器