文档介绍：学校代码： 10385 分类号：
研究生学号： 1000201046 密级：

硕士学位论文

指令表程序的形式化验证方法研究
Research on Formal Methods for Verifying
Instruction List Program

作者姓名：齐鹏飞
指导教师：罗继亮副教授
学科：控制科学与工程
研究方向：离散事件动态系统
所在学院：信息科学与工程学院

论文提交日期：二零一三年三月二十八日
学位论文独创性声明
本人声明兹呈交的学位论文是本人在导师指导下完成的研究成
果。论文写作中不包含其他人已经发表或撰写过的研究内容，如参考
他人或集体的科研成果，均在论文中以明确的方式说明。本人依法享
有和承担由此论文所产生的权利和责任。

论文作者签名：签名日期：

学位论文版权使用授权声明
本人同意授权华侨大学有权保留并向国家机关或机构送交学位论
文的复印件和电子版，允许学位论文被查阅和借阅。本人授权华侨大
学可以将本学位论文的全部内容或部分内容编入有关数据库进行检
索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。

论文作者签名：指导教师签名：
签名日期：签名日期：
摘要
摘要
随着计算机技术、网络通信技术的高速发展，社会需求量的不断增大，国
家对工业自动化水平的要求也在不断提高。作为目前一项非常重要的自动化技
术，可编程逻辑控制器（Programmable Logic Controller，PLC）的广泛应用为企
业提供了巨大的帮助，尤其是在传统继电器控制系统的数控化改造过程中，PLC
更是起到了不可替代的作用。但是，生产事故的不断发生为社会敲响了警钟。
企业在不断追求自动化技术的同时，对其可靠性的要求也应该不断提升。
在这一需求下，学术界开展了大量关于如何提高自动化控制程序可靠性的
研究。目前，传统的PLC程序检测方法还存在明显不足，更多的是针对语法、语
义的检测，而针对程序变量间逻辑关系的检测却少之又少。为了弥补这一不足，
形式化验证方法逐渐走入了研究者的视野。形式化验证方法主要包括演绎验证
和模型检测两大类。相比较演绎验证，模型检测技术能够自动化地完成这一工
作。本文就是在这样一个大背景下诞生的，提出了一种用于指令表程序的形式
化验证方法：
1．选用Petri网作为PLC指令表程序的建模工具，提出将指令表程序自动地
转换为Petri网模型的相关算法；
2．选用计算树逻辑语言描述PLC指令表程序所控制系统的控制规范；
3．选用NuSMV模型检测器对已建立的Petri网模型以及计算树逻辑语言进行
模型检测。其中包含了将Petri网模型转换为SMV程序的方法，以及对系统状态
空间爆炸问题的简化处理；
4．根据模型检测的结果有针对性的修改存在问题的指令表程序。
本文旨在通过上述方法，提高PLC指令表程序的可靠性，减少其在实际生产
应用中潜在的安全隐患，为企业实现自动化控制提供有力的帮助。
关键词：指令表 Petri网模