| 摘要 | 第5-6页 |
| Abstract | 第6页 |
| 第一章 绪论 | 第9-18页 |
| 1.1 研究背景及意义 | 第9-10页 |
| 1.2 研究现状 | 第10-14页 |
| 1.2.1 PLC程序验证研究现状 | 第10-12页 |
| 1.2.2 PLC程序生成研究现状 | 第12-14页 |
| 1.2.3 存在问题分析 | 第14页 |
| 1.3 论文工作 | 第14-16页 |
| 1.4 论文组织结构 | 第16-18页 |
| 第二章 相关理论与技术 | 第18-33页 |
| 2.1 可编程控制器PLC | 第18-22页 |
| 2.1.1 PLC的工作原理 | 第18-19页 |
| 2.1.2 PLC编程语言 | 第19-22页 |
| 2.2 定理证明工具Coq | 第22-29页 |
| 2.2.1 表达式、类型和函数 | 第22页 |
| 2.2.2 命题和证明 | 第22-23页 |
| 2.2.3 基础逻辑 | 第23-24页 |
| 2.2.4 归纳数据类型和归纳证明 | 第24-27页 |
| 2.2.5 证明策略和自动化证明 | 第27-29页 |
| 2.3 线性时序逻辑LTL | 第29-30页 |
| 2.4 未来区间逻辑FIL | 第30-32页 |
| 2.4.1 FIL语法 | 第31-32页 |
| 2.4.2 FIL语义 | 第32页 |
| 2.5 本章小结 | 第32-33页 |
| 第三章 PLC程序的正确性证明 | 第33-43页 |
| 3.1 定理证明方法简介 | 第33页 |
| 3.2 IL语法在Coq中的定义 | 第33-35页 |
| 3.3 IL操作语义在Coq中的定义 | 第35-39页 |
| 3.3.1 IL指令的语义在Coq中的定义 | 第35-38页 |
| 3.3.2 IL程序语义在Coq中的定义 | 第38-39页 |
| 3.4 PLC自锁控制程序的正确性证明 | 第39-41页 |
| 3.5 证明的自动化 | 第41-42页 |
| 3.6 本章小结 | 第42-43页 |
| 第四章 SPS到FIL的转换 | 第43-52页 |
| 4.1 时序规约模式系统SPS | 第43-46页 |
| 4.1.1 Scope在状态序列模型上的形式化定义 | 第44-45页 |
| 4.1.2 Property在状态序列模型上的形式化定义 | 第45-46页 |
| 4.2 SPS到FIL的转换 | 第46-49页 |
| 4.3 证明SPS到FIL转换的正确性 | 第49-51页 |
| 4.4 本章小结 | 第51-52页 |
| 第五章 面向SPS的PLC程序生成 | 第52-75页 |
| 5.1 SPS规约描述语言 | 第52-53页 |
| 5.2 SPS的可实现化及其PLC实现 | 第53-57页 |
| 5.3 SPS的组合式程序生成 | 第57-64页 |
| 5.3.1 SPS的程序组合规则 | 第57-60页 |
| 5.3.2 SPS的程序生成示例 | 第60-64页 |
| 5.4 SPS规约系统的程序生成 | 第64-74页 |
| 5.4.1 SPS规约系统的程序组合规则 | 第64-69页 |
| 5.4.2 SPS规约系统的程序生成示例 | 第69-74页 |
| 5.5 本章小结 | 第74-75页 |
| 第六章 总结与展望 | 第75-77页 |
| 6.1 主要内容总结 | 第75页 |
| 6.2 未来工作展望 | 第75-77页 |
| 致谢 | 第77-78页 |
| 参考文献 | 第78-82页 |
| 附录 A 属性模式的PLC程序实现 | 第82-85页 |
| 附录 B 范围模式的PLC程序实现 | 第85页 |