基于形式化方法的PLC程序设计与验证研究综述
在安全苛求工程领域中可编程逻辑控制器（PLC）的可靠性需求的驱动下，近年来学术界开展了大量的PLC程序的形式化设计和验证方法研究。本文列举了它们在核电、列车和导弹控制系统等工程的应用；总结了现有PLC形式化设计和验证方法的研究方法：在形式化设计方面，介绍了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果；在形式化验证方面，介绍了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法；分析比较了现有研究方法中优势与不足，展望了有望取得突破的研究方向。
可编程逻辑控制器 程序设计 Petri网 自动机模型
齐鹏飞 罗继亮 陈雪琨
华侨大学信息科学与工程学院, 厦门 361021
国内会议
厦门
中文
1-6
2012-08-01（万方平台首次上网日期，不代表论文的发表时间）