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

Automating the Generation of Test Sequences from B Formal Specification

基于严格数学理论的软件形式化规格说明,经过逐层精化,不仅可以让软件开发过程更加有效精准,而且为测试用例测试序列的自动生成提供了最原始可靠的依据。通过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.