基于形式规约的软件测试用例自动生成技术研究

Research on Automatic Test Case Generation Based on Form Specification

在Hierons提出的一种基于Z语言软件自动测试方法的基础上进行了拓展.该方法基于软件的Z语言规约;以Hierons提出的推理规则为基础,提出了分裂树的算法,将操作模式的约束条件转换为形如∨iPi∧Qi的析取范式;然后根据析取范式将Z语言描述的操作模式划分为子操作模式;依据子操作模式的前置条件和后置条件,将子操作模式作为状态转换图的转换关系,构建了被测试软件的状态转换图;依据状态转换图,提出了相应的状态覆盖准则、转换关系覆盖准则和转换关系谓词覆盖准则等测试数据选择准则.

This paper extended Hierons′ automatic test case generated from Z specification. Based on Hierons′s rewrite rules and Z specification, a tree split arithmetic was presented to rewrite the restriction predication in Operation Scheme to ∨iP_i∧Q_i disjunctive normal form. With this disjunctive normal form, the Operation Scheme written in Z was divided into Sub-Operation Scheme. According to Sub-Operation Scheme′s pre-condition and post-condition, Sub-Operation Scheme was used as state graph′s transition. Then a finite state automation model (FSM) was derived. According to the FSM, test criterion, such as state coverage adequacy criterion, transition coverage adequacy criterion and transition predication coverage criterion were also presented.