形式化B描述测试序列自动生成研究  

Automating the Generation of Test Sequences from B Formal Specification

作　　者：丁岳伟[1] 彭金梅[1] 

机构地区：[1]上海理工大学光电信息与计算机工程学院,上海200093

出　　处：《计算机系统应用》2012年第5期77-81,共5页Computer Systems & Applications

摘　　要：基于严格数学理论的软件形式化规格说明,经过逐层精化,不仅可以让软件开发过程更加有效精准,而且为测试用例测试序列的自动生成提供了最原始可靠的依据。通过B抽象机操作的规范型,依据测试理论,可以将原操作等价于多个效用谓词(effect predication)的形式。按照路径覆盖得到状态转换图,并对状态图做了确定性处理;运用基于状态图的测试准则,生成有效的测试序列,提高测试的有效性和效率。Formal specification,based on critical mathematics,not only make the process of software development more effective and precise,but also contain a great deal of information that can be as the original reliable basis for the generation of test sequences.The work reported here base on the standard B notation,splitting the operation to the equal effect predications and then generate state transition diagram according to path coverage criterion,and also solving the indeterminism of state transition.Generating the test sequences according to the test criterion on the state diagram,which can prove an effective test,has also been presented.

关 键 词：形式化描述 测试序列生成 状态转换图 B方法 效用谓词 

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