论文题目: 基于实时规约的测试预言自动生成技术的研究
论文类型: 博士论文
论文专业: 计算机科学与技术
作者: 王馨
导师: 齐治昌
关键词: 侧试预言,带接收状态的时间自动机,度量区间时序逻辑,最差情况执行时间
文献来源: 国防科学技术大学
发表年度: 2005
论文摘要: 实时系统目前已广泛应用于工业、军事和民用高科技的各个领域，其中，航空航天、医疗监控、军事指挥和武器装备控制等领域对实时系统的安全性和实时性要求非常高。一旦软件控制出现问题，后果往往不堪设想。为此，实时软件在正式投入使用之前，必须保证其正确性。实时系统的显著特性是对系统的时序性要求严格。由于实时逻辑语义精确、对实时系统时序性质描述能力强大、测试和验证算法便捷，因此日益受到软件工程领域研究人员和系统工程师们的重视。 鉴于人们对高质量软件的迫切需求，以软件测试为中心的质量保障技术在软件生产实践中得到了迅速发展和广泛应用，已成为发现软件缺陷、保证软件质量的关键技术之一。测试预言（test oracle）是检验待测系统在特定执行下是否正确运行的方法，也是软件测试过程中的重要环节。本文提出了基于受限度量区间时序逻辑（Metric Interval Temporal Logic，MITL）的测试预言自动生成技术。首先针对MITL[0，b]的语法和语义，使用模型检验中的tableau思想，通过使用重写规则，将一条线性因果的MITL[0，b]逻辑公式自动转换为带接收状态的时间自动机（Timed Automata with Accepting States，TAAS），由时间自动机充当测试预言。然后，在此基础上对实时规约的表达能力进行扩充，针对MITL[a，6]的语法和语义，提出相应的测试预言自动生成算法。 由于生成的时间自动机是非确定的，因此，充当测试预言的自动机的状态空间对于检验实时系统的效率起着决定作用，状态空间越大、迁移越多，运行时的系统开销越大。为此，本文提出对时间自动机进行优化的方法，尽可能地减少冗余状态、去除不可达状态。此外，本文还对带时标的状态序列的精化过程提出优化方法，在一定程度上缩减了由精化产生的额外状态-区间对。 测试预言以实时系统的轨迹作为输入。获取轨迹的方法有两种，要么在系统外部进行监测，要么在系统内部插入断言并输出。两种方法各有利弊，外部监测不会打扰系统运行但可观测的内容受限，而断言的插入则会打扰实时系统的实际运行，进而可能改变系统的时间特性。本文提出一种折衷的方法，根据规约的内容选择获取轨迹的方法，该方法是上述两种方法的综合，力图吸取上述两种方法的长处，而回避两者的不足。使用最差情况执行时间（Worst Case Execution Time，WCET）分析技术，对插入的断言开销进行了分析，进而对由于断言的插入而导致对系统时间的影响提出补偿方法。 我们设计并实现了一个Windows环境下的测试预言自动生成工具AutoTO，能够将以MITL书写的实时系统规约自动地转换为可执行的测试预言。
论文目录:
摘要
ABSTRACT
第一章 绪论
§1．1 实时系统
§1．2 形式化方法
§1．3 软件测试与测试预言
§1．4 本文的主要研究内容
§1．5 本文的结构
第二章 测试预言技术
§2．1 用于转换器的预言
§2．2 基于嵌入式断言的测试预言
2．2．1 预处理器方法
2．2．2 直接程序编码方法
2．2．3 小结
§2．3 基于外部接口契约的测试预言
2．3．1 专用接口契约
2．3．2 现有规约符号的修改
2．3．3 小结
§2．4 轨迹检验与日志文件分析
2．4．1 轨迹检验
2．4．2 日志文件分析
2．4．3 小结
§2．5 基于形式化规约的测试预言
2．5．1 基于Z和Object-Z的测试预言自动生成技术
2．5．2 基于时序逻辑的测试预言生成技术
2．5．3 基于时间自动机的测试预言
2．5．4 SCR方法
2．5．5 基于petri网的测试预言生成技术
2．5．6 多语言规约
§2．6 存在的问题与未来发展方向
第三章 实时规约与时间自动机
§3．1 实时系统与形式化规约
3．1．1 实时系统的时序约束
3．1．2 形式化规约
§3．2 实时规约
3．2．1 实时规约的时间域
3．2．2 实时规约MITL
§3．3 时间自动机
第四章 基于MITL_([0,b])的测试预言自动生成
§4．1 实时规约MITL_([0,b])
§4．2 基于MITL_([0,b])的测试预言自动生成
4．2．1 时间自动机的构造思想
4．2．2 扩展的MITL_([0,b])(EMITL_([0,b]))
4．2．3 正规形式与重写规则
4．2．4 带接收状态的时间自动机的构建
4．2．5 算法的复杂性分析
§4．3 示例
第五章 基于MITL_([a,b])的测试预言自动生成
§5．1 实时规约MITL_([a,b])
§5．2 测试预言自动生成算法
5．2．1 测试预言构造思想的扩展
5．2．2 扩展的MITL_([a,b])(EMITL_([a,b]))
5．2．3 正规形式与重写规则
5．2．4 带接收状态的时间自动机的构建
5．2．5 算法的复杂性分析
§5．3 示例
第六章 测试预言自动生成技术的优化
§6．1 时间自动机的优化
§6．2 φ-fine过程的优化
第七章 实时系统行为轨迹的获取
§7．1 WECT分析技术
§7．2 实时系统的轨迹获取
7．2．1 基于规约内容和系统特性的轨迹获取
7．2．2 新的轨迹获取方式对实时系统时间行为的影响
§7．3 插装断言的时间分析和补偿
7．3．1 插装断言对被测系统的时间影响分析
7．3．2 插装断言的构造
7．3．3 插装断言的时间计算
7．3．4 目标系统的时间计算和修正
§7．4 示例
7．4．1 模型简介
7．4．2 实验环境
7．4．3 模拟程序
7．4．4 时间计算
7．4．5 实验结果
第八章 测试预言自动生成工具的设计与实现
§8．1 AutoTO的体系结构
§8．2 AutoTO的设计与实现
8．2．1 系统用例图
8．2．2 系统设计
8．2．3 顺序图
8．2．4 实验结果
第九章 结束语
§9．1 本文的主要贡献
§9．2 下一步研究工作
致谢
攻读博士学位期间发表的论文
参考文献
发布时间: 2006-09-22
相关论文
- [1].面向路径的测试数据自动生成方法研究[D]. 单锦辉.国防科学技术大学2002
- [2].并发系统的模型检测与测试[D]. 吴鹏.中国科学院研究生院（软件研究所）2005
- [3].基于UML的软件统计测试研究[D]. 颜炯.国防科学技术大学2005
- [4].Web应用软件的测试技术研究[D]. 路晓丽.西北大学2006
- [5].依赖性分析及其在软件测试中的应用[D]. 缪力.湖南大学2006
- [6].高可信软件可靠性和防危性测试与评价理论研究[D]. 覃志东.电子科技大学2005
- [7].软件测试与可靠性评估[D]. 张广梅.中国科学院研究生院（计算技术研究所）2006
- [8].软件测试方法研究[D]. 赵瑞莲.中国科学院研究生院（计算技术研究所）2001
- [9].测试数据自动生成技术研究[D]. 史亮.东南大学2006
- [10].基于软件体系结构的测试用例生成技术研究[D]. 叶俊民.哈尔滨工程大学2005
标签：侧试预言论文; 带接收状态的时间自动机论文; 度量区间时序逻辑论文; 最差情况执行时间论文;