Test Case Generation from Conjunctions of Predicates with Model Checking  

作　　者：TIAN Cong LIU Shaoying DUAN Zhenhua 

机构地区：[1]ICTT and ISN Lab, Xidian University [2]Department of Computer Science, Hosei University

出　　处：《Chinese Journal of Electronics》2014年第2期271-277,共7页电子学报（英文版）

基　　金：supported by the Hosei University HIF Fellowship;the National Natural Science Foundation of China(No.61003078,No.61133001,No.61272117,and No.91218301);the National Basic Research Program of China(973 Program)(No.2010CB328102);ISN Lab(No.ISN1102001)

摘　　要：Automatic test case generation from a prepost style formal specification must deal with the issue of how to generate test cases from a conjunction of atomic predicate expressions, but unfortunately this problem has not been effectively solved due to its intrinsic difficulty. We describe a practical approach to tackling this problem by utilizing the model checking technique. An algorithm that converts test case generation from a conjunction of atomic predicate expressions into model checking is proposed. We discuss how the algorithm deals with atomic predicate expressions involving only variables of numeric types, and extend the discussion to variables of compound types such as set, sequence, and composite types. Case studies are presented to assess the feasibility and effectiveness of our approach.Automatic test case generation from a pre- post style formal specification must deal with the issue of how to generate test cases from a conjunction of atomic predicate expressions, but unfortunately this problem has not been effectively solved due to its intrinsic difficulty. We describe a practical approach to tackling this problem by utilizing the model checking technique. An algorithm that converts test case generation from a conjunction of atomic predicate expressions into model checking is proposed. We discuss how the algorithm deals with atomic predicate ex- pressions involving only variables of numeric types, and extend the discussion to variables of compound types such as set, sequence, and composite types. Case studies are presented to assess the feasibility and effectiveness of our approach.

关 键 词：Model checking TESTING Testing cases. 

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