基于MSVL的动静结合程序验证和自动规划

目录

声明

插图索引

表格索引

符号对照表

缩略语对照表

第一章 绪论

1.1 研究背景和现状

1.2 本文的研究目的和主要工作

1.3 论文的组织结构

第二章 技术背景

2.1 投影时序逻辑

2.2 建模、仿真和验证语言

2.3 命题投影时序逻辑

2.4 本章小结

第三章 MSVL编译器

3.1 MSVL程序编译

3.2 仿真和建模

3.3 实例

3.4 本章小结

第四章 基于MSVL的动静结合程序验证

4.1 基于反例的抽象精化

4.2 方法框架

4.3 算法实现

4.4 实现和实验

4.5 本章小结

第五章 完全正则时序性质挖掘

5.1 方法框架

5.2 算法实现

5.3 方法示例

5.4 并行挖掘

5.5 本章小结

第六章 基于MSVL的自动规划

6.2 规划问题建模

6.3 搜索控制知识描述

6.4 实验分析

6.5 本章小结

第七章 总结与展望

7.2 研究展望

参考文献

致谢

作者简介