PLC程序形式化的设计与验证

Design and Verification on the PLC Program Based on Formal Methods

从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法.最后,比较将两种形式化方法应用到PLC程序的特点,探讨现有成果中存在的问题及研究发展方向.

From the perspective of formal methods, this paper states lots of researches on the formal design and verification of programmable logic controllers （PLC） programs. As for formal design, the proposed methods, which are to judge whether PLC programs are correct and reliable based on Petri nets or automata, are depicted. As for formal verification, it is summarized that how to model PLC programs as Petri nets, and how to verify PLC programs using NuSMV or UPPAAL. At last, the advantages and disadvantages of these reported approaches are stated, and the research directions which are expected to breakthrough, are pointed out.