| 摘要 | 第3-4页 |
| Abstract | 第4页 |
| 第1章 绪论 | 第8-14页 |
| 1.1 课题研究背景与意义 | 第8-10页 |
| 1.1.1 选题依据 | 第8-9页 |
| 1.1.2 形式化方法介绍 | 第9-10页 |
| 1.2 国内外研究现状 | 第10-12页 |
| 1.3 本文研究内容以及结构安排 | 第12-14页 |
| 第2章 基础知识 | 第14-24页 |
| 2.1 引言 | 第14页 |
| 2.2 梯形图指令介绍 | 第14-17页 |
| 2.3 Petri 网基础知识 | 第17-21页 |
| 2.3.1 Petri 网的基本概念 | 第17-18页 |
| 2.3.2 Petri 网的重要性质 | 第18-19页 |
| 2.3.3 Petri 网的分析方法 | 第19-21页 |
| 2.4 模型检测器 NuSMV 基础知识 | 第21-23页 |
| 2.4.1 计算树逻辑（ Computation Tree Logic ，CTL） | 第21页 |
| 2.4.2 模型检测器 NuSMV | 第21-23页 |
| 2.5 本章小结 | 第23-24页 |
| 第3章 梯形图定时器的 Petri 网建模方法 | 第24-44页 |
| 3.1 引言 | 第24页 |
| 3.2 PLC 定时器分类以及工作原理简介 | 第24-26页 |
| 3.3 基于普通 Petri 网定时器建模算法 | 第26-40页 |
| 3.3.1 建模原理 | 第26页 |
| 3.3.2 算法流程图 | 第26-28页 |
| 3.3.3 算法具体内容 | 第28-33页 |
| 3.3.4 实例分析 | 第33-40页 |
| 3.4 定时器 Petri 网模型的封装 | 第40-43页 |
| 3.4.1 封装原理 | 第40-42页 |
| 3.4.2 封装目的 | 第42-43页 |
| 3.5 文章小结 | 第43-44页 |
| 第4章 梯形图功能指令的 Petri 网建模方法 | 第44-65页 |
| 4.1 引言 | 第44页 |
| 4.2 梯形图功能指令及其工作原理简介 | 第44-46页 |
| 4.3 基于普通 Petri 网的比较指令建模算法 | 第46-52页 |
| 4.3.1 建模的基本原理 | 第46-47页 |
| 4.3.2 算法具体内容 | 第47-51页 |
| 4.3.3 实例分析 | 第51-52页 |
| 4.4 基于普通 Petri 网的数学运算指令建模算法 | 第52-57页 |
| 4.4.1 建模的基本原理 | 第52页 |
| 4.4.2 加(减)法运算指令的 Petri 网建模算法 | 第52-56页 |
| 4.4.3 实例分析 | 第56-57页 |
| 4.5 其他功能指令的 Petri 网建模方法 | 第57-64页 |
| 4.5.1 移位和循环移位指令的 Petri 网建模 | 第57-60页 |
| 4.5.2 其他指令的 Petri 网建模 | 第60-64页 |
| 4.6 本章小结 | 第64-65页 |
| 第5章 梯形图程序顺序规范的检测方法 | 第65-72页 |
| 5.1 引言 | 第65页 |
| 5.2 梯形图程序“顺序”规范的检测方法 | 第65-68页 |
| 5.2.1 “顺序”规范检测原理 | 第66页 |
| 5.2.2 Petri 网模型转化为 NuSMV 程序的算法 | 第66-68页 |
| 5.2.3 具体方法 | 第68页 |
| 5.3 实例分析 | 第68-71页 |
| 5.5 本章小结 | 第71-72页 |
| 第6章 梯形图程序的形式化验证方法在实际系统的应用 | 第72-80页 |
| 6.1 引言 | 第72页 |
| 6.2 应用背景 | 第72-77页 |
| 6.2.1 自动化仓库的工作原理 | 第72-73页 |
| 6.2.2 自动化仓库的控制要求 | 第73页 |
| 6.2.3 基于 S7-200 的自动化仓库的 PLC 程序 | 第73-77页 |
| 6.3 自动化仓库的 Petri 网模型 | 第77页 |
| 6.4 对自动化仓库梯形图程序的“顺序”规范检测 | 第77-79页 |
| 6.5 本章小结 | 第79-80页 |
| 第7章 总结与展望 | 第80-82页 |
| 7.1 文章总结 | 第80-81页 |
| 7.2 展望未来 | 第81-82页 |
| 参考文献 | 第82-86页 |
| 致谢 | 第86-88页 |
| 个人简历、在学期间发表的学术论文及研究成果 | 第88页 |
