首页/ 上海红神信息技术有限公司/ 专利详情

PLC程序到NuSMV输入模型的自动化构建方法

基本信息

申请号 CN201710382639.4 申请日 -
公开（公告）号 CN107193745B 公开（公告）日 2019-10-29
申请公布号 CN107193745B 申请公布日 2019-10-29
分类号 G06F11/36;G05B19/05 分类 计算；推算；计数;
发明人 魏强;常天佑;麻荣宽;耿洋洋;刘雯雯 申请（专利权）人 上海红神信息技术有限公司
代理机构 郑州大通专利商标代理有限公司 代理人 陈大通
地址 450000 河南省郑州市高新区科学大道62号
法律状态 -

摘要

摘要 本发明涉及工业自动化控制技术领域，特别是涉及一种PLC程序到NuSMV输入模型的自动化构建方法，包括对PLC的ST语言进行分析，构建ST语言的语法；根据给出的ST语法对ST程序进行处理，将ST程序解析为抽象语法树AST；对抽象语法树AST进行处理，分析ST语言语句的控制流特征，确定各语句生成控制流图CFG的算法；根据控制流图CFG对ST程序进行数据流分析，构建状态转换邻接表和变量取值变化邻接表；根据构建的状态转换邻接表和变量取值变化邻接表生成NuSMV输入模型。本发明大大提高NuSMV工具对PLC程序进行模型检测的效率和准确度，实现对工业控制系统PLC代码的安全性验证。