一种基于SAT求解器的符号模型检测方法、检测系统及其应用
公开
摘要
本发明公开了一种基于SAT求解器的符号模型检测方法：读取待检测文件，将待检测文件解析为C++程序中对应的数据结构存储用于后续步骤，得到待检测模型M和待检测安全性性质P，将待检测安全性质P取反得到不安全性性质bad；待检测安全性性质P由线性时态逻辑编写；将待检测模型M蕴含的状态以及状态间的迁移关系构造为文字和等价的子句，存入SAT求解器供后续步骤使用；将当前状态si以及不安全性性质bad作为假设，在待检测模型M的子句集合约束下进行求解，若公式可满足，则从当前状态si可以一步到达违反安全性质的坏状态；从初始状态到坏状态的路径，即为目击者或反例，作为证明系统不安全的证据。
基本信息
专利标题 ：
一种基于SAT求解器的符号模型检测方法、检测系统及其应用
专利标题（英）：
暂无
公开（公告）号 ：
CN114564202A
申请号 ：
CN202210038442.X
公开（公告）日 ：
2022-05-31
申请日 ：
2022-01-13
授权号 ：
暂无
授权日 ：
暂无
发明人 ：
于忠祺李建文张小禹蒲戈光
申请人 ：
华东师范大学;上海工业控制安全创新科技有限公司
申请人地址 ：
上海市闵行区东川路500号
代理机构 ：
上海德禾翰通律师事务所
代理人 ：
夏思秋
优先权 ：
CN202210038442.X
主分类号 ：
G06F8/41
IPC分类号 ：
G06F8/41
IPC结构图谱
G
G部——物理
G06
计算；推算或计数
G06F
电数字数据处理
G06F8/00
软件工程设计
G06F8/40
程序代码转换
G06F8/41
编译
法律状态
2022-05-31 ：
公开
注：本法律状态信息仅供参考，即时准确的法律状态信息须到国家知识产权局办理专利登记簿副本。
文件下载
暂无PDF文件可下载
