%0 Journal Article
%T PLC程序形式化的设计与验证
%A 罗继亮
%A 陈雪琨
%A 齐鹏飞
%J 华侨大学学报(自然科学版)
%D 2013
%R 10.11830/ISSN.1000-5013.2013.03.0241
%X 从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法.最后,比较将两种形式化方法应用到PLC程序的特点,探讨现有成果中存在的问题及研究发展方向.
%K 可编程逻辑控制器
%K 形式化设计
%K Petri网
%K 自动机
%K 定理证明
%K 模型验证
%U http://www.hdxb.hqu.edu.cn/oa/DArticle.aspx?type=view&id=201303001