程序时序属性的自动测试  

Testing of Temporal Properties of Program

作　　者：马晓东[1] 董威[1] 王戟[1] 齐治昌[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机科学》2004年第6期132-134,179,共4页Computer Science

摘　　要：测试预言是一种用来检测被测系统的测试执行是否正确的方法。文中,作者设计并实现了一种根据程序的线性时序逻辑(LTL)的性质产生测试预言的方法。首先,作者将一线性时序逻辑公式转换为一个有限状态自动机,然后,管理源代码,以便抽取与线性时序逻辑性质有关的状态序列。最后,用该信息来模拟状态自动机,并决定程序执行是否满足线性时序逻辑的性质。Test oracle is a method of checking whether the system under test has behaved correctly on a particular execution. In this paper, we design and implement a method of producing test oracle from program's LTL(Linear Temporal Logic) property. First, we transfer a LTL formula to a finite state automaton; then, we manage the source code in order to extract state sequence which is relative to the LTL property; in the end, we use this information to stimulate the automaton and decide whether the execution of the program satisfies the LTL property.

关 键 词：测试预言 线性时序逻辑 FSA LTL 状态自动机 反应式系统 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]