计算机科学

计算机科学 ›› 2023, Vol. 50 ›› Issue (6): 297-306.doi: 10.11896/jsjkx.220500207

• 信息安全 • 上一篇    下一篇

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

张泽伦1,2, 杨志斌1,2, 李晓劼1,2, 周勇1,2, 李维3   

  1. 1 南京航空航天大学计算机科学与技术学院 南京 211106
    2 高安全系统的软件开发与验证技术工信部重点实验室 南京 211106
    3 航空防护救生技术航空科技重点实验室 湖北 襄阳 441003
  • 收稿日期:2022-05-23 修回日期:2022-09-13 出版日期:2023-06-15 发布日期:2023-06-06
  • 通讯作者: 杨志斌(yangzhibin168@163.com)
  • 作者简介:(zhangzelun@nuaa.edu.cn)
  • 基金资助:
    国家自然科学基金(62072233);国防基础科研项目(JCKY2020205C006);航空科学基金(201919052002)

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

ZHANG Zelun1,2, YANG Zhibin1,2, LI Xiaojie1,2, ZHOU Yong1,2, LI Wei3   

  1. 1 School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China
    2 Key Laboratory of Safety-critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China
    3 Aviation Key Laboratory of Science and Technology on Life-support Technology,Xiangyang,Hubei 441003,China
  • Received:2022-05-23 Revised:2022-09-13 Online:2023-06-15 Published:2023-06-06
  • About author:ZHANG Zelun,born in 1998,postgra-duate,is a member of China Computer Federation.His main research interests include safety-critical systems and formal verification.YANG Zhibin,born in 1982,Ph.D,professor,is a member of China Computer Federation.His main research interests include safety-critical system,formal verification and AI software enginee-ring.
  • Supported by:
    National Natural Science Foundation of China(62072233),National Defense Basic Scientific Research Project(JCKY2020205C006) and Aeronautical Science Foundation of China(201919052002).

PDF (PC)

540

摘要： 高安全应用开发环境(Safety Critical Application Development Environment,SCADE)是工业界进行安全关键软件建模、仿真测试和形式化验证的常用工具,如何解决工业级软件的SCADE模型在进行形式化验证时遇到的状态空间爆炸问题是目前面临的一项重要挑战。基于契约的组合验证方法通过研究软件各构件的上下文和外部环境来编写环境假设对构件的状态空间进行约束,能够解决状态空间爆炸问题,但环境假设的手工编写费时费力。为了解决这一问题,文中提出了一种基于机器学习的SCADE模型组合验证环境假设自动生成方法。首先,针对SCADE模型采用自动仿真方法生成机器学习方法所需数据集;然后,采用决策树和遗传算法进行环境假设自动生成;最后,实现了具有SCADE模型分析和环境假设自动生成功能的原型工具,并基于弹射座椅控制系统案例,验证了所提方法的有效性。

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

Abstract: 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.

Key words: SCADE, Compositional verification, Environment assumption, Decision tree, Genetic algorithm

中图分类号: 

  • TP311
[1]LEVESON N.Engineering a Safer World:Systems ThinkingApplied to Safety[M].Massachusetts:MIT Press,2011.
[2]RIERSON L.Developing safety-critical software:a practicalguide for aviation software and DO-178c complia[M].Taylor &Francis,2013.
[3]Radio Technical Commission Aeronautics.Model-based development and verification supplement to DO-178C and DO-278A:DO-331[S].Washington DC:Radio Technical Commission Aeronautics,2011.
[4]Radio Technical Commission Aeronautics.Formal methods supplement to DO-178C and DO-278A:DO-333[S].Washington DC:Radio Technical Commission Aeronautics,2011.
[5]JING H,SHEN Y Y.ANSYS SCADE Suite Modeling Foundation [M].Beijing:China Water Resources and Hydropower Press,2018.
[6]COFER D,GACEK A,MILLER S,et al.Compositional verification of architectural models[C]//NASA Formal Methods Symposium.Berlin:Springer,2012:126-140.
[7]BENVENISTE A,CAILLAUD B,NICKOVIC D,et al.Con-tracts for systems design:Theory[D].Paris;INRIA,2015.
[8]NUZZO P.Compositional design of cyber-physical systems using contracts[D].Berkeley:UC Berkeley,2015.
[9]LI Z B,LI Q B,YU L,et al.Survey on Adaptive Random Testing by Partitioning[J].Computer Science,2019,46(3):19-29.
[10]LI L X,WANG H F,QI Z H,et al.Vehicle ATP Test CaseGeneration Method Based on SCADE Model[J].Journal of the China Railway Society,2020,42(9):102-110.
[11]BAO X A,XIONG Z J,ZHANG W,et al.Approach for Path-oriented Test Cases Generation Based on Improved Genetic Algorithm[J].Computer Science,2018,45(8):174-178.
[12]HUANG Y Y,LI F Y,CHANG L,et al.Symbolic ZBDD-based Generation Algorithm for Combinatorial Testing[J].Computer Science,2018,45(1):255-260.
[13]TANG L,LI F.Research on Forecasting Model of Internet of Vehicles Security Situation Based on Decision Tree[J].Compu-ter Science,2021,48(6A):514-517.
[14]LI Y,CAO T,JANSEN D N,et al.Accelerated Verification of Parametric Protocols with Decision Trees[C]//International Conference on Computer Design.IEEE,2020:397-404.
[15]ZOU J,ZHU G S,QI X Y,et al.HTTPS Encrypted Traffic Classification Method Based on C4.5 Decision Tree[J].Compu-ter Science,2020,47(6A):381-385.
[16]RICCARDO P,WILLIAM B L,NICHOLAS F.McPhee:A Field Guide to Genetic Programming[J].Genetic Programming and Evolvable Machines,2009,10(2):229-230.
[17]MEYER B.Applying ‘design by contract'[J].Computer,1992,25(10):40-51.
[18]MEYER B.Touch of Class:Learning to Program Well with Objects and Contracts[M].Springer Publishing Company,Incorporated,2009.
[19]JONES C B.Specification and design of(parallel) programs[C]//9th IFIP World Computer Congress(Information Proces-sing 83).Newcastle University,1983.
[20]ABADI M,LAMPORT L.Conjoining specifications[J].ACM Transactions on Programming Languages and Systems(TOPLAS),1995,17(3):507-535.
[21]KOMURAVELLI A,PĂSĂREANU C S,CLARKE E M.Assume-guarantee abstraction refinement for probabilistic systems[C]//International Conference on Computer Aided Verification.Berlin:Springer,2012:310-326.
[22]WARMER J B,KLEPPE A G.The object constraint language:getting your models ready for MDA[M].Boston:Addison-Wesley Professional,2003.
[23]ALFARO L, HENZINGER T T A.Interface theories for component-based design[C]//International Workshop on Embedded Software.Berlin:Springer,Heidelberg,2001:148-165.
[24]DERLER P,LEE E A,TRIPAKIS S,et al.Cyber-physical system design contracts[C]//Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems.2013:109-118.
[25] COBLEIGH J M,GIANNAKOPOULOU D,PASAREANU CS.Learning Assumptions for Compositional Verification[C]//Tools and Algorithms for the Construction and Analysis of Systems.2003:331-346.
[26]GIANNAKOPOULOU D,PASAREANU C S,BARRINGERH.Assumption generation for software component verification[C]//Proceedings 17th IEEE International Conference on Automated Software Engineering.IEEE,2002:3-12.
[27]GAALOUL K,MENGHI C,NEJATI S,et al.Mining assumptions for software components using machine learning[C]//Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering.2020:159-171.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市渝北区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发