基于状态转换的PLC程序模型构建方法
来源：计算机应用杂志2017年第12期北京时间：
作者：常天佑, 魏强, 耿洋洋
单位：1. 信息工程大学, 郑州 450001;2. 数学工程与先进计算国家重点实验室, 郑州 450001
摘要：针对可编程逻辑控制器（PLC）程序在进行NuSMV模型检测时需要手工对程序进行建模，不仅浪费人力且容易出错的问题，提出一种基于状态转移的PLC程序模型自动化构建方法。该方法首先分析结构化文本（ST）语言特性并解析ST程序为抽象语法树；其次，在抽象语法树基础上，根据不同的文法结构进行控制流分析生成控制流图；然后，通过数据流分析得到程序依赖图；最后，根据程序依赖图生成NuSMV的输入模型。实验结果表明，所提方法实现了ST程序到NuSMV输入模型的自动化构建，并且构建的NuSMV输入模型既保留了ST程序的原有特性又符合NuSMV模型检测工具输入的规范，与传统手工模型构建方法相比，提高了模型生成的效率和准确率。
关键词：工业控制系统安全,模型检测,NuSMV,程序分析,模型构建
基金资助：国家重点研发计划项目（2016YFB0800203）；上海市科研计划项目（14DZ1104800）。
