Efficient representation for formal verification of PLC programs
Efficient representation for formal verification of PLC programs
复制标题
PLC 程序形式化验证的有效表示
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Jean
中科院分区：
文献类型：
--
作者：
V. Gourcuff;O. D. Smet;Jean
本文讨论了使用NuSMV模型检查器进行模型检测的可扩展性。为了避免或至少限制组合爆炸，提出了一种高效的PLC程序表示方法。该表示只包括对属性证明有意义的状态。描述了一种将结构化文本中开发的PLC程序转换为基于该表示的NuSMV模型的方法，并通过几个例子进行了举例说明。将用该方法构建的模型得到的结果、状态空间大小和验证时间与以前发表的方法得到的结果进行了比较，以评估所提出的表示的效率
This paper addresses scalability of model-checking using the NuSMV model-checker. To avoid or at least limit combinatory explosion, an efficient representation of PLC programs is proposed. This representation includes only the states that are meaningful for properties proof. A method to translate PLC programs developed in structured text into NuSMV models based on this representation is described and exemplified on several examples. The results, state space size and verification time, obtained with models constructed using this method are compared to those obtained with previously published methods so as to assess efficiency of the proposed representation