| 摘要 | 第1-11页 |
| ABSTRACT | 第11-13页 |
| 第一章 绪论 | 第13-23页 |
| §1．1 实时系统 | 第14-15页 |
| §1．2 形式化方法 | 第15-17页 |
| §1．3 软件测试与测试预言 | 第17-19页 |
| §1．4 本文的主要研究内容 | 第19-21页 |
| §1．5 本文的结构 | 第21-23页 |
| 第二章 测试预言技术 | 第23-45页 |
| §2．1 用于转换器的预言 | 第24-25页 |
| §2．2 基于嵌入式断言的测试预言 | 第25-28页 |
| 2．2．1 预处理器方法 | 第26-27页 |
| 2．2．2 直接程序编码方法 | 第27页 |
| 2．2．3 小结 | 第27-28页 |
| §2．3 基于外部接口契约的测试预言 | 第28-30页 |
| 2．3．1 专用接口契约 | 第28-29页 |
| 2．3．2 现有规约符号的修改 | 第29-30页 |
| 2．3．3 小结 | 第30页 |
| §2．4 轨迹检验与日志文件分析 | 第30-32页 |
| 2．4．1 轨迹检验 | 第31页 |
| 2．4．2 日志文件分析 | 第31-32页 |
| 2．4．3 小结 | 第32页 |
| §2．5 基于形式化规约的测试预言 | 第32-42页 |
| 2．5．1 基于Z和Object-Z的测试预言自动生成技术 | 第32-33页 |
| 2．5．2 基于时序逻辑的测试预言生成技术 | 第33-39页 |
| 2．5．3 基于时间自动机的测试预言 | 第39-40页 |
| 2．5．4 SCR方法 | 第40页 |
| 2．5．5 基于petri网的测试预言生成技术 | 第40-42页 |
| 2．5．6 多语言规约 | 第42页 |
| §2．6 存在的问题与未来发展方向 | 第42-45页 |
| 第三章 实时规约与时间自动机 | 第45-59页 |
| §3．1 实时系统与形式化规约 | 第45-49页 |
| 3．1．1 实时系统的时序约束 | 第45-47页 |
| 3．1．2 形式化规约 | 第47-49页 |
| §3．2 实时规约 | 第49-54页 |
| 3．2．1 实时规约的时间域 | 第49-52页 |
| 3．2．2 实时规约MITL | 第52-54页 |
| §3．3 时间自动机 | 第54-59页 |
| 第四章 基于MITL_([0,b])的测试预言自动生成 | 第59-88页 |
| §4．1 实时规约MITL_([0,b]) | 第59-62页 |
| §4．2 基于MITL_([0,b])的测试预言自动生成 | 第62-83页 |
| 4．2．1 时间自动机的构造思想 | 第62-66页 |
| 4．2．2 扩展的MITL_([0,b])(EMITL_([0,b])) | 第66-74页 |
| 4．2．3 正规形式与重写规则 | 第74-76页 |
| 4．2．4 带接收状态的时间自动机的构建 | 第76-81页 |
| 4．2．5 算法的复杂性分析 | 第81-83页 |
| §4．3 示例 | 第83-88页 |
| 第五章 基于MITL_([a,b])的测试预言自动生成 | 第88-109页 |
| §5．1 实时规约MITL_([a,b]) | 第88-90页 |
| §5．2 测试预言自动生成算法 | 第90-106页 |
| 5．2．1 测试预言构造思想的扩展 | 第90-91页 |
| 5．2．2 扩展的MITL_([a,b])(EMITL_([a,b])) | 第91-98页 |
| 5．2．3 正规形式与重写规则 | 第98-100页 |
| 5．2．4 带接收状态的时间自动机的构建 | 第100-104页 |
| 5．2．5 算法的复杂性分析 | 第104-106页 |
| §5．3 示例 | 第106-109页 |
| 第六章 测试预言自动生成技术的优化 | 第109-117页 |
| §6．1 时间自动机的优化 | 第109-115页 |
| §6．2 φ-fine过程的优化 | 第115-117页 |
| 第七章 实时系统行为轨迹的获取 | 第117-133页 |
| §7．1 WECT分析技术 | 第117-118页 |
| §7．2 实时系统的轨迹获取 | 第118-122页 |
| 7．2．1 基于规约内容和系统特性的轨迹获取 | 第120-121页 |
| 7．2．2 新的轨迹获取方式对实时系统时间行为的影响 | 第121-122页 |
| §7．3 插装断言的时间分析和补偿 | 第122-128页 |
| 7．3．1 插装断言对被测系统的时间影响分析 | 第122-124页 |
| 7．3．2 插装断言的构造 | 第124-126页 |
| 7．3．3 插装断言的时间计算 | 第126-127页 |
| 7．3．4 目标系统的时间计算和修正 | 第127-128页 |
| §7．4 示例 | 第128-133页 |
| 7．4．1 模型简介 | 第128-129页 |
| 7．4．2 实验环境 | 第129页 |
| 7．4．3 模拟程序 | 第129-131页 |
| 7．4．4 时间计算 | 第131页 |
| 7．4．5 实验结果 | 第131-133页 |
| 第八章 测试预言自动生成工具的设计与实现 | 第133-139页 |
| §8．1 AutoTO的体系结构 | 第133-134页 |
| §8．2 AutoTO的设计与实现 | 第134-139页 |
| 8．2．1 系统用例图 | 第134-135页 |
| 8．2．2 系统设计 | 第135-137页 |
| 8．2．3 顺序图 | 第137页 |
| 8．2．4 实验结果 | 第137-139页 |
| 第九章 结束语 | 第139-142页 |
| §9．1 本文的主要贡献 | 第139-140页 |
| §9．2 下一步研究工作 | 第140-142页 |
| 致谢 | 第142-144页 |
| 攻读博士学位期间发表的论文 | 第144-145页 |
| 参考文献 | 第145-164页 |
