基于形式化方法的PLC程序设计与验证研究综述

摘要

在安全苛求工程领域中可编程逻辑控制器（PLC）的可靠性需求的驱动下，近年来学术界开展了大量的PLC程序的形式化设计和验证方法研究。本文列举了它们在核电、列车和导弹控制系统等工程的应用；总结了现有PLC形式化设计和验证方法的研究方法：在形式化设计方面，介绍了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果；在形式化验证方面，介绍了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法；分析比较了现有研究方法中优势与不足，展望了有望取得突破的研究方向。