基于自然语言需求的SCADE模型测试用例自动生成方法  

Natural Language Requirements Based Approach for Automatic Test Cases Generation of SCADE Models

作　　者：邵温欣 杨志斌[1,2] 李维 周勇 SHAO Wenxin;YANG Zhibin;LI Wei;ZHOU Yong(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Key Laboratory of Safety-critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China;Aviation Key Laboratory of Science and Technology on Life-support Technology,Xiangyang,Hubei 441003,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]高安全系统的软件开发与验证技术工信部重点实验室,南京211106 [3]航空防护救生技术航空科技重点实验室,湖北襄阳441003

出　　处：《计算机科学》2024年第7期29-39,共11页Computer Science

基　　金：国家自然科学基金(62072233);国防基础科研项目(JCKY2020205C006);航空科学基金(201919052002);南京航空航天大学科研与实践创新计划(xcxjh20221607)。

摘　　要：随着安全关键软件规模和复杂性不断增加,模型驱动开发方法在安全关键领域得到了广泛应用。SCADE作为一种重要的建模方法和工具,能够表达确定性并发行为且具有精确时间语义等特性,适用于安全关键软件的建模、测试与验证。目前,已有方法主要采用手工方式构造SCADE模型测试用例,存在需求与测试用例不一致、成本代价高且容易出错的问题。文中提出了一种基于自然语言需求的SCADE模型测试用例自动生成方法。首先,给出了基于模型检测的测试用例自动生成方法,通过自然语言需求处理生成原子命题,用于生成前提假设Assume和观察者模型,同时给出了陷阱性质(Trap Properties)生成规则来生成陷阱性质用于模型检测;其次,给出了基于覆盖分析和变异测试的测试用例质量评估方法,并在SCADE模型上进行变异测试;最后,设计和实现了原型工具,并基于一个工业界案例飞行员弹射座椅控制系统进行了案例分析,验证了所提方法的有效性。With the increasing scale and complexity of safety-critical software,model-driven development(MDD)is widely used in safety-critical fields.As an important modeling method and tool,SCADE can express deterministic concurrent behavior and has precise time semantics,which is suitable for modeling,testing and verification of safety-critical software.At present,the existing methods mainly use manual methods to construct SCADE model test cases,and there are some problems such as inconsistency between requirements and test cases,high cost and easy to make mistakes.This paper presents an automatic generation method of SCADE model test cases based on natural language requirements.Firstly,an automatic test case generation method based on mo-del checking is presented,which generates atomic propositions by natural language requirements processing to generate the assume and observer models,and provides the rules of trap properties generation to generate trap properties for model checking.Secondly,a test case quality evaluation method based on coverage analysis and mutation testing is presented,and the mutation testing is carried out on SCADE model.Finally,the prototype tool is designed and implemented,and an industrial case of pilot ejection seat control system is analyzed to verify the effectiveness of the proposed method.

关 键 词：安全关键软件 模型驱动开发 SCADE 测试用例自动生成 模型检测 

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