PLC系统及其FBD编程语言的形式化建模与实时性验证
| 摘要 | 第3-4页 |
| Abstract | 第4-5页 |
| 第1章 绪论 | 第9-19页 |
| 1.1 概述 | 第9-11页 |
| 1.2 研究现况和分析 | 第11-14页 |
| 1.2.1 PLC系统形式化建模与验证的研究现况 | 第11-13页 |
| 1.2.2 现状分析 | 第13-14页 |
| 1.3 PLC系统与FBD编程语言 | 第14-16页 |
| 1.3.1 PLC系统结构 | 第14-15页 |
| 1.3.2 IEC61131-3 标准 | 第15页 |
| 1.3.3 FBD编程语言 | 第15-16页 |
| 1.3.4 FBD的优势 | 第16页 |
| 1.4 论文内容和章节安排 | 第16-18页 |
| 1.5 本章小节 | 第18-19页 |
| 第2章 目标模型和时态逻辑 | 第19-30页 |
| 2.1 形式化方法探索 | 第19-21页 |
| 2.1.1 形式化建模方法 | 第19-20页 |
| 2.1.2 形式化验证方法 | 第20-21页 |
| 2.2 目标模型的研究 | 第21-26页 |
| 2.2.1 UML模型 | 第22页 |
| 2.2.2 Petri网模型 | 第22-23页 |
| 2.2.3 自动机模型 | 第23-26页 |
| 2.3 时态逻辑公式 | 第26-29页 |
| 2.3.1 CTL（计算树逻辑） | 第26-27页 |
| 2.3.2 TCTL（时间计算树逻辑） | 第27-28页 |
| 2.3.3 时态逻辑的选择 | 第28-29页 |
| 2.4 本章小结 | 第29-30页 |
| 第3章 基于时间自动机的PLC系统建模 | 第30-49页 |
| 3.1 PLC系统建模框架 | 第30-31页 |
| 3.2 中间形式的表示 | 第31-33页 |
| 3.3 单一指令建模 | 第33-40页 |
| 3.3.1 逻辑运算指令 | 第33-35页 |
| 3.3.2 定时器指令 | 第35-37页 |
| 3.3.3 计数器指令 | 第37页 |
| 3.3.4 算术运算指令 | 第37-38页 |
| 3.3.5 跳转指令 | 第38-39页 |
| 3.3.6 比较指令 | 第39-40页 |
| 3.3.7 传送指令 | 第40页 |
| 3.4 其余部分建模 | 第40-43页 |
| 3.4.1 协调模块 | 第41页 |
| 3.4.2 外部环境模块 | 第41-42页 |
| 3.4.3 循环控制模块 | 第42-43页 |
| 3.5 模块组合算法 | 第43-47页 |
| 3.5.1 算法的理论基础 | 第43-44页 |
| 3.5.2 形式化描述 | 第44-45页 |
| 3.5.3 算法的流程图 | 第45-47页 |
| 3.6 本章小结 | 第47-49页 |
| 第4章 应用研究 | 第49-62页 |
| 4.1 时效正确性性质 | 第49-50页 |
| 4.2 验证工具UPPAAL介绍 | 第50-53页 |
| 4.2.1 基本功能 | 第50-51页 |
| 4.2.2 语言规范 | 第51-52页 |
| 4.2.3 最新改进 | 第52-53页 |
| 4.3 验证过程 | 第53-54页 |
| 4.3.1 模型验证步骤 | 第53页 |
| 4.3.2 建模标准 | 第53-54页 |
| 4.4 传送带系统 | 第54-60页 |
| 4.4.1 实例描述 | 第54-56页 |
| 4.4.2 模型建立 | 第56-59页 |
| 4.4.3 验证与结论 | 第59-60页 |
| 4.5 本章小结 | 第60-62页 |
| 第5章 结论与展望 | 第62-64页 |
| 5.1 工作总结与创新点 | 第62-63页 |
| 5.2 未来工作展望 | 第63-64页 |
| 参考文献 | 第64-67页 |
| 致谢 | 第67-69页 |
| 个人简历 | 第69页 |
