程序时序属性的自动测试

Testing of Temporal Properties of Program

测试预言是一种用来检测被测系统的测试执行是否正确的方法。文中,作者设计并实现了一种根据程序的线性时序逻辑(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.