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

doi:10.11772/j.issn.1001-9081.2017.12.3574

计算机应用 ›› 2017, Vol. 37 ›› Issue (12): 3574-3580.DOI: 10.11772/j.issn.1001-9081.2017.12.3574

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

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

1. 信息工程大学, 郑州 450001;
2. 数学工程与先进计算国家重点实验室, 郑州 450001

收稿日期:2017-06-13 修回日期:2017-09-07 出版日期:2017-12-10 发布日期:2017-12-18
通讯作者: 常天佑
作者简介:常天佑(1992-),男,河南驻马店人,硕士研究生,主要研究方向:工控安全;魏强(1979-),男,江西南昌人,教授,博士,主要研究方向:软件脆弱性分析、工控安全;耿洋洋(1994-),男,河南周口人,硕士研究生,主要研究方向:工控安全。
基金资助:
国家重点研发计划项目（2016YFB0800203）；上海市科研计划项目（14DZ1104800）。

Constructing method of PLC program model based on state transition

CHANG Tianyou^1,2, WEI Qiang^1,2, GENG Yangyang^1,2

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).

摘要/Abstract

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

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

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程序模型构建方法[J]. 计算机应用, 2017, 37(12): 3574-3580.

CHANG Tianyou, WEI Qiang, GENG Yangyang. Constructing method of PLC program model based on state transition[J]. Journal of Computer Applications, 2017, 37(12): 3574-3580.

参考文献

[1] MCLAUGHLIN S. On dynamic malware payloads aimed at programmable logic controllers[C]//Proceedings of the 20116th USENIX Conference on Hot Topics in Security. Berkeley, CA:USENIX Association, 2011:1-6.
[2] KLICK J, LAU S, MARZIN D, et al. Internet-facing PLCs-a new back orifice[EB/OL].[2017-04-16]. http://www.inf.fu-berlin.de/inst/ag-si/pub/us-15-Klick-Internet-Facing-PLCs-A-New-Back-Orifice-paper.pdf.
[3] SPENNEBERG R, BRVGGEMANN M, SCHWARTKE H. PLC-blaster:a worm living solely in the PLC[EB/OL].[2017-04-16]. http://regmedia.co.uk/2016/04/29/plc_87458745.pdf.
[4] LARSEN K G, PETTERSSON P, WANG Y, et al. UPPAAL in a nutshell[J]. International Journal on Software Tools for Technology Transfer, 1997, 1(1/2):134-152.
[5] YOVINE S. KRONOS:a verification tool for real-time systems[J]. International Journal on Software Tools for Technology Transfer, 1997, 1(1/2):123-133.
[6] HAVELUND K, PENIX J, VISSER W. SPIN model checking and software verification[C]//Proceedings of the 20007th International SPIN Workshop on Model Checking of Software, LNCS 1885. Berlin:Springer, 2000:655-659.
[7] CIMATTI A, CLARKE E, GIUNCHIGLIA F, et al. NuSMV:a new symbolic model verifier[C]//Proceedings of the 1999 International Conference on Computer Aided Verification, LNCS 1633. Berlin:Springer, 1999:495-499.
[8] SZPYRKA M, A BIERNACKA, BIERNACKI J. Methods of translation of Petri nets to NuSMV language[C/OL]//Proceedings of the 201423th International Workshop on Concurrency, Specification and Programming,[2017-04-16]. http://www.ceur-ws.org/Vol-1269/paper245.pdf.
[9] ADIEGO B F, DARVAS D, TOURNIER J C, et al. Automated Generation of Formal Models from ST Control Programs for Verification Purposes, CERN-ACC-NOTE-2014-0037[R]. Geneva, Switzerland:CERN, 2014.
[10] 肖力田,顾明,孙家广.一种PLC程序语言指称语义及函数的形式化定义方法[J].中南大学学报(自然科学版),2011,42(增刊1):1107-1113. (XIAO L T, GU M, SUN J G. Formal definition method of denotational semantics and functions for PLC program language[J]. Journal of Central South University (Science and Technology), 2011, 42(Suppl. 1):1107-1113.)
[11] MCLAUGHLIN S, ZONOUZ S, POHLY D, et al. A trusted safety verifier for process controller code[EB/OL].[2017-04-16]. http://adambates.org/courses/cs598-fa16/slides/cs598-17-slides-trusted-safety-verifier.pdf.
[12] BIHA S O. A formal semantics of PLC programs in Coq[C]//Proceedings of the 2011 IEEE 35th Annual Computer Software and Applications Conference. Washington, DC:IEEE Computer Society, 2011:118-127.

[1]	包玉龙, 朱雪阳, 张文辉, 孙鹏飞, 赵颖琪. 物联网应用中访问控制智能合约的形式化验证[J]. 计算机应用, 2021, 41(4): 930-938.
[2]	安鑫, 夏近伟, 杨海娇, 欧阳一鸣, 任福继. 基于离散控制器合成的异构多核系统资源管理方法[J]. 计算机应用, 2020, 40(6): 1698-1706.
[3]	毛昕怡, 钮俊, 丁雪儿, 张开乐. 基于模型检测的微服务组合平台QoS验证[J]. 计算机应用, 2020, 40(11): 3267-3272.
[4]	贾尚坤, 贺飞. 基于证据自动机的软件回归验证[J]. 计算机应用, 2018, 38(10): 2990-2995.
[5]	刘洁瑞, 巫雪青, 严俊, 杨红丽. 针对Android资源泄漏的基准测试集的构造与评测[J]. 计算机应用, 2017, 37(4): 1129-1134.
[6]	于丽贞徐中伟陈祖希张舒青. 基于梯形逻辑的联锁系统形式化验证方法[J]. 计算机应用, 2013, 33(12): 3419-3422.
[7]	廖紫骅谭红艳吴尽昭. 基于Groebner基的模型检测技术及其工具实现[J]. 计算机应用, 2009, 29(10): 2841-2843.
[8]	陈晨陈永生. 基于层次单元划分的软件模型检测技术研究[J]. 计算机应用, 2008, 28(8): 2109-2112.
[9]	闫志华李成郑艳萍. 工作流模型检测研究[J]. 计算机应用, 2007, 27(6): 1448-1451.
[10]	文英董荣胜郭云川. 一种提高Ad Hoc网络节点能量效率的DPM模型[J]. 计算机应用, 2007, 27(5): 1095-1098.
[11]	缪力张大方. 程序模型检测的两阶段框架[J]. 计算机应用, 2007, (12): 3089-3091.
[12]	张频罗贵明 . UML模型检测方法的研究[J]. 计算机应用, 2007, 27(10): 2493-2497.
[13]	姜洋罗贵明 . Petri网模型的扩展与检测[J]. 计算机应用, 2007, 27(1): 183-185.
[14]	熊贻青 . 针对微软中间语言的逆向分析[J]. 计算机应用, 2006, 26(7): 1523-1525.
[15]	张斌罗贵明王平 . 一种有效的基于LTL和Petri网的模型检测方法[J]. 计算机应用, 2006, 26(10): 2490-2493.

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

Constructing method of PLC program model based on state transition

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics