Abstract: The Programmable Logic Controller (PLC) program needs modeling the program manually in the NuSMV model testing, which is not only a waste of manpower but also an error-prone procedure. In order to solve the problems, an automatic construction method of PLC program model based on state transition was proposed. Firstly, the Structured Text (ST) language features were analyzed and the ST program was parsed as an abstract grammar tree. Secondly, according to the abstract grammar tree, the control flow graph was generated based on different grammatical structure by control flow analysis. And then the program dependency graph was obtained by data flow analysis. Finally, the NuSMV input model was generated according to the program dependency graph. The experimental results shows that, the proposed method achieves the automatic construction from ST program to NuSMV input model, and the constructed NuSMV input model not only retains the original characteristics of ST program but also conforms to the input standard of NuSMV model detection tool. Compared with the traditional manual model construction method, the proposed method improves the efficiency and accuracy of model generation.

Key words: industrial control system security, model detection, NuSMV, program analysis, model constructing

摘要： 针对可编程逻辑控制器（PLC）程序在进行NuSMV模型检测时需要手工对程序进行建模，不仅浪费人力且容易出错的问题，提出一种基于状态转移的PLC程序模型自动化构建方法。该方法首先分析结构化文本（ST）语言特性并解析ST程序为抽象语法树；其次，在抽象语法树基础上，根据不同的文法结构进行控制流分析生成控制流图；然后，通过数据流分析得到程序依赖图；最后，根据程序依赖图生成NuSMV的输入模型。实验结果表明，所提方法实现了ST程序到NuSMV输入模型的自动化构建，并且构建的NuSMV输入模型既保留了ST程序的原有特性又符合NuSMV模型检测工具输入的规范，与传统手工模型构建方法相比，提高了模型生成的效率和准确率。

关键词: 工业控制系统安全, 模型检测, NuSMV, 程序分析, 模型构建