深圳摇号申请网站,模块化网站建设 局域网,wordpress的官方网,外贸公司网站空间在2024-2025学期的巴黎高师同步反应式系统(2024-2025)第三课中#xff0c;详细讨论了基于SMT的Lustre模型检查器Kind 2的工作。本文将提供对Kind 2的介绍。对课程的详细内容#xff0c;可参考同步反应式系统 简介
本节课讨论了基于SMT#xff08;Satisfiability Modulo The… 在2024-2025学期的巴黎高师同步反应式系统(2024-2025)第三课中详细讨论了基于SMT的Lustre模型检查器Kind 2的工作。本文将提供对Kind 2的介绍。对课程的详细内容可参考同步反应式系统 简介
本节课讨论了基于SMTSatisfiability 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模型检查器
