公开(公告)号：CN114356294B

公开(公告)日：2023-07-14

申请号：CN202111570950.4

申请日：2021-12-21

申请人： 华东师范大学 ,  卡斯柯信号有限公司 ,  上海工业控制安全创新科技有限公司

发明人： 陈羽 ,  李建文 ,  张小禹 ,  蒲戈光 ,  王燕芩 ,  李卫娟 ,  张程 ,  魏民 ,  朱迎春 ,  张铭瑶

IPC分类号： G06F8/30

摘要： 本发明公开了一种基于FQLTL的实例生成方法，本方法获取系统设备集合、设备性质以及设备间关系等配置信息，通过遍历公式的语法树进行逻辑计算，判断每个对象/对象集合是否满足公式中所限定的范围，由最终得到的逻辑运算结果可以滤去恒真/恒假的集合,这些集合都无需进行下一步验证，留下真正需要验证的设备集合，也就是状态不确定的设备集合。包括如下步骤：对公式进行语法解析；预处理；遍历语法树，进行可满足性检查；输出可满足性检查结果。由于验证器无法进行包含范围的性质验证，而这种新的形式化语言中规定了需要验证集合的范围。故本发明解决了在验证项目中，从系统全部的设备集合缩减到真正待验证实例的问题。

公开(公告)号：CN114356294A

公开(公告)日：2022-04-15

申请号：CN202111570950.4

申请日：2021-12-21

申请人： 华东师范大学 ,  卡斯柯信号有限公司 ,  上海工业控制安全创新科技有限公司

发明人： 陈羽 ,  李建文 ,  张小禹 ,  蒲戈光 ,  王燕芩 ,  李卫娟 ,  张程 ,  魏民 ,  朱迎春 ,  张铭瑶

IPC分类号： G06F8/30

摘要： 本发明公开了一种基于FQLTL的实例生成方法，本方法获取系统设备集合、设备性质以及设备间关系等配置信息，通过遍历公式的语法树进行逻辑计算，判断每个对象/对象集合是否满足公式中所限定的范围，由最终得到的逻辑运算结果可以滤去恒真/恒假的集合,这些集合都无需进行下一步验证，留下真正需要验证的设备集合，也就是状态不确定的设备集合。包括如下步骤：对公式进行语法解析；预处理；遍历语法树，进行可满足性检查；输出可满足性检查结果。由于验证器无法进行包含范围的性质验证，而这种新的形式化语言中规定了需要验证集合的范围。故本发明解决了在验证项目中，从系统全部的设备集合缩减到真正待验证实例的问题。

公开(公告)号：CN114564202A

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

申请号：CN202210038442.X

申请日：2022-01-13

申请人： 华东师范大学 ,  上海工业控制安全创新科技有限公司

发明人： 于忠祺 ,  李建文 ,  张小禹 ,  蒲戈光

IPC分类号： G06F8/41

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

公开(公告)号：CN114564202B

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

申请号：CN202210038442.X

申请日：2022-01-13

申请人： 华东师范大学 ,  上海工业控制安全创新科技有限公司

发明人： 于忠祺 ,  李建文 ,  张小禹 ,  蒲戈光

IPC分类号： G06F8/41

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