一种基于SAT求解器的符号模型检测方法、检测系统及其应用

摘要

本发明公开了一种基于SAT求解器的符号模型检测方法：读取待检测文件，将待检测文件解析为C++程序中对应的数据结构存储用于后续步骤，得到待检测模型M和待检测安全性性质P，将待检测安全性质P取反得到不安全性性质bad；待检测安全性性质P由线性时态逻辑编写；将待检测模型M蕴含的状态以及状态间的迁移关系构造为文字和等价的子句，存入SAT求解器供后续步骤使用；将当前状态si以及不安全性性质bad作为假设，在待检测模型M的子句集合约束下进行求解，若公式可满足，则从当前状态si可以一步到达违反安全性质的坏状态；从初始状态到坏状态的路径，即为目击者或反例，作为证明系统不安全的证据。