论文部分内容阅读
实时系统目前已广泛应用于工业、军事和民用高科技的各个领域,其中,航空航天、医疗监控、军事指挥和武器装备控制等领域对实时系统的安全性和实时性要求非常高。一旦软件控制出现问题,后果往往不堪设想。为此,实时软件在正式投入使用之前,必须保证其正确性。实时系统的显著特性是对系统的时序性要求严格。由于实时逻辑语义精确、对实时系统时序性质描述能力强大、测试和验证算法便捷,因此日益受到软件工程领域研究人员和系统工程师们的重视。 鉴于人们对高质量软件的迫切需求,以软件测试为中心的质量保障技术在软件生产实践中得到了迅速发展和广泛应用,已成为发现软件缺陷、保证软件质量的关键技术之一。测试预言(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书写的实时系统规约自动地转换为可执行的测试预言。