基于机器学习的SCADE模型组合验证环境假设自动生成方法  

Machine Learning Based Environment Assumption Automatic Generation for Compositional Verification of SCADE Models

作　　者：张泽伦 杨志斌[1,2] 李晓劼 周勇 李维[3] ZHANG Zelun;YANG Zhibin;LI Xiaojie;ZHOU Yong;LI Wei(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

出　　处：《计算机科学》2023年第6期297-306,共10页Computer Science

基　　金：国家自然科学基金(62072233);国防基础科研项目(JCKY2020205C006);航空科学基金(201919052002)。

摘　　要：高安全应用开发环境(Safety Critical Application Development Environment, SCADE)是工业界进行安全关键软件建模、仿真测试和形式化验证的常用工具,如何解决工业级软件的SCADE模型在进行形式化验证时遇到的状态空间爆炸问题是目前面临的一项重要挑战。基于契约的组合验证方法通过研究软件各构件的上下文和外部环境来编写环境假设对构件的状态空间进行约束,能够解决状态空间爆炸问题,但环境假设的手工编写费时费力。为了解决这一问题,文中提出了一种基于机器学习的SCADE模型组合验证环境假设自动生成方法。首先,针对SCADE模型采用自动仿真方法生成机器学习方法所需数据集;然后,采用决策树和遗传算法进行环境假设自动生成;最后,实现了具有SCADE模型分析和环境假设自动生成功能的原型工具,并基于弹射座椅控制系统案例,验证了所提方法的有效性。Safety critical application development environment(SCADE)is a common tool in industry for modeling,simulation,testing and verification of the safety-critical software.How to solve the state space explosion problem in formal verification of the SCADE model is an important challenge.The contract-based compositional verification method solves this problem by learning the context and external environment of each component of the software,then using environmental assumptions to constrain the state space of components,but manually obtaining of environmental assumptions is time-consuming and labor-intensive.This paper proposes an environment assumption automatic generation method for SCADE model.First,an automatic simulation method is used for the SCADE model to generate the data set required for the machine learning method.Secondly,the decision tree and genetic algorithm are used to generate environmental assumptions automatically.Finally,a prototype tool with SCADE model analysis and environment assumption automatic generation is implemented,and the ejection seat control system is used as a case to verify the effectiveness of the proposed method.

关 键 词：SCADE 组合验证 环境假设 决策树 遗传算法 

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