一种基于FQLTL语言的实例生成方法及系统

本发明公开了一种基于FQLTL的实例生成方法，本方法获取系统设备集合、设备性质以及设备间关系等配置信息，通过遍历公式的语法树进行逻辑计算，判断每个对象/对象集合是否满足公式中所限定的范围，由最终得到的逻辑运算结果可以滤去恒真/恒假的集合,这些集合都无需进行下一步验证，留下真正需要验证的设备集合，也就是状态不确定的设备集合。包括如下步骤：对公式进行语法解析；预处理；遍历语法树，进行可满足性检查；输出可满足性检查结果。由于验证器无法进行包含范围的性质验证，而这种新的形式化语言中规定了需要验证集合的范围。故本发明解决了在验证项目中，从系统全部的设备集合缩减到真正待验证实例的问题。
华东师范大学 | 卡斯柯信号有限公司 | 上海工业控制安全创新科技有限公司
陈羽 | 李建文 | 张小禹 | 蒲戈光 | 王燕芩 | 李卫娟 | 张程 | 魏民 | 朱迎春 | 张铭瑶