%0 Journal Article
%T 程序时序属性的自动测试
%A 马晓东 董威 王戟 齐治昌？
%J 计算机科学
%D 2004
%X 测试预言是一种用来检测被测系统的测试执行是否正确的方法。文中，作者设计并实现了一种根据程序的线性时序逻辑(ltl)的性质产生测试预言的方法。首先，作者将一线性时序逻辑公式转换为一个有限状态自动机，然后，管理源代码，以便抽取与线性时序逻辑性质有关的状态序列。最后，用谊信息来模拟状态自动机，并决定程序执行是否满足线性时序逻辑的性质。
%K 测试预言线性时序逻辑fsaltl状态自动机反应式系统
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=10707140&flag=1