一种基于形式化描述的测试案例生成方法  

Test cases generation based on formal specification

作　　者：丁洪达[1,2] 王伟光[1,2] 曾庆凯[1,2] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,江苏南京210093 [2]南京大学计算机科学与技术系,江苏南京210093

出　　处：《解放军理工大学学报（自然科学版）》2009年第4期318-323,共6页Journal of PLA University of Science and Technology(Natural Science Edition)

基　　金：国家自然科学基金资助项目(60773170;60721002;90818022);国家863计划资助项目(2006AA01Z432);高等学校博士学科点专项科研基金资助项目(200802840002)

摘　　要：基于形式化描述的验证测试是高安全系统的有效评估方法,而如何生成测试案例是基于形式化测试中的关键问题。针对形式化方法生成测试案例的不足,在分析形式化描述语言Z结构特点的基础上,提出了一种基于形式化描述的测试案例生成方法。从分析Z语言描述的输入空间、前置条件和后置条件出发,对前置条件适当重写,然后根据前置条件利用更改的判定条件覆盖准则来生成测试案例集,该方法引入了控制流覆盖准则,克服了经验方法输入空间划分不完整的缺点,降低了形式化描述的难度,并可以使测试案例生成过程自动化。Validating testing based on formal How to generate test cases on formal specific existing approaches, a novel approach to test control-flow coverage criteria was adopted incompletely. It can reduce the difficulties automatically. specifiation fication is an effective is a key cases generat to solve the in designing problem. By ion based on problem that way in evaluating secure systems. analyzing the disadvantages of the Z specification was proposed. The the input space was partitioned formal specification and generate test cases

关 键 词：安全评估 安全测试 形式化方法 测试案例生成 覆盖准则 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]