公开(公告)号：CN114564202B

公开(公告)日：2023-02-17

申请号：CN202210038442.X

申请日：2022-01-13

Applicant: 华东师范大学 ,  上海工业控制安全创新科技有限公司

Inventor： 于忠祺 ,  李建文 ,  张小禹 ,  蒲戈光

IPC: G06F8/41

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

公开(公告)号：CN114564202A

公开(公告)日：2022-05-31

申请号：CN202210038442.X

申请日：2022-01-13

Applicant: 华东师范大学 ,  上海工业控制安全创新科技有限公司

Inventor： 于忠祺 ,  李建文 ,  张小禹 ,  蒲戈光

IPC: G06F8/41

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