论文部分内容阅读
可编程逻辑控制器（Programmable Logic Controller，PLC）是工业自动化的一种重要的控制装置，在一些安全苛求的行业中（例如在交通、电力和化工石油等）被广泛使用，这就对PLC程序的安全可靠性提出了严格的要求。然而传统的PLC程序开发工具仅能识别语义和语法问题，却无法检测出隐藏在程序中的逻辑错误。为此，很多学者展开了对PLC程序进行逻辑错误检测的研究工作，取得了丰硕的成果。其中，形式化验证方法为学术界广泛认可。本文基于Petri网给出了PLC梯形图程序进行建模方法，以及Petri网模型和模型检测工具NuSMV相结合的梯形图顺序规范验证方法：1.根据国际电工委员会标准IEC61131-3定义的语义，将多种梯形图功能指令转换为普通Petri网，其中包括定时器、比较和加法指令；2.采用计算树逻辑（Computation Tree Logic，CTL）公式描述梯形图程序的“顺序”规范；3.将PLC程序的Petri网模型和CTL顺序规范输入模型检测工具NuSMV，进行程序验证；4.根据验证结果对存在问题的梯形图程序进行相应的修改。该方法可以自动识别和定位梯形图中违反顺序规范的逻辑错误，能够提高PLC系统的可靠性和安全性，对PLC程序的设计和调试具有较大的应用价值。