Journal of Computer Applications ›› 2017, Vol. 37 ›› Issue (12): 3574-3580.DOI: 10.11772/j.issn.1001-9081.2017.12.3574

Previous Articles     Next Articles

Constructing method of PLC program model based on state transition

CHANG Tianyou1,2, WEI Qiang1,2, GENG Yangyang1,2   

  1. 1. Information Engineering University, Zhengzhou Henan 450001, China;
    2. State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou Henan 450001, China
  • Received:2017-06-13 Revised:2017-09-07 Online:2017-12-10 Published:2017-12-18
  • Supported by:
    This work is partially supported by the National Key Research and Development Program of China (2016YFB0800203), the Scientific Research Plan Program of Shanghai (14DZ1104800).

基于状态转换的PLC程序模型构建方法

常天佑1,2, 魏强1,2, 耿洋洋1,2   

  1. 1. 信息工程大学, 郑州 450001;
    2. 数学工程与先进计算国家重点实验室, 郑州 450001
  • 通讯作者: 常天佑
  • 作者简介:常天佑(1992-),男,河南驻马店人,硕士研究生,主要研究方向:工控安全;魏强(1979-),男,江西南昌人,教授,博士,主要研究方向:软件脆弱性分析、工控安全;耿洋洋(1994-),男,河南周口人,硕士研究生,主要研究方向:工控安全。
  • 基金资助:
    国家重点研发计划项目(2016YFB0800203);上海市科研计划项目(14DZ1104800)。

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, 程序分析, 模型构建

CLC Number: