Computer Science

Computer Science ›› 2023, Vol. 50 ›› Issue (6): 297-306.doi: 10.11896/jsjkx.220500207

• Computer Network • Previous Articles     Next Articles

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)

241

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

CLC Number: 

  • 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.
[1] BAI Mingli, WANG Mingwen. Fabric Defect Detection Algorithm Based on Improved Cascade R-CNN [J]. Computer Science, 2023, 50(6A): 220300224-6.
[2] KE Haiping, MAO Yijun, GU Wanrong. Recommendation Model Based on Decision Tree and Improved Deep & Cross Network [J]. Computer Science, 2023, 50(6A): 220300084-7.
[3] REN Gaoke, MO Xiuliang. Network Security Situation Assessment for GA-LightGBM Based on PRF-RFECV Feature Optimization [J]. Computer Science, 2023, 50(6A): 220400151-6.
[4] SHI Liang, WEN Liangming, LEI Sheng, LI Jianhui. Virtual Machine Consolidation Algorithm Based on Decision Tree and Improved Q-learning by Uniform Distribution [J]. Computer Science, 2023, 50(6): 36-44.
[5] ZHONG Jialin, WU Yahui, DENG Su, ZHOU Haohao, MA Wubin. Multi-objective Federated Learning Evolutionary Algorithm Based on Improved NSGA-III [J]. Computer Science, 2023, 50(4): 333-342.
[6] SHANG Yuye, YUAN Jiabin. Task Offloading Method Based on Cloud-Edge-End Cooperation in Deep Space Environment [J]. Computer Science, 2023, 50(2): 80-88.
[7] YUE Qing, YIN Jian-yu, WANG Sheng-sheng. Automatic Detection of Pulmonary Nodules in Low-dose CT Images Based on Improved CNN [J]. Computer Science, 2022, 49(6A): 54-59.
[8] YANG Hao-xiong, GAO Jing, SHAO En-lu. Vehicle Routing Problem with Time Window of Takeaway Food ConsideringOne-order-multi-product Order Delivery [J]. Computer Science, 2022, 49(6A): 191-198.
[9] SHAO Yan-hua, LI Wen-feng, ZHANG Xiao-qiang, CHU Hong-yu, RAO Yun-bo, CHEN Lu. Aerial Violence Recognition Based on Spatial-Temporal Graph Convolutional Networks and Attention Model [J]. Computer Science, 2022, 49(6): 254-261.
[10] SHAO Yu, CHEN Ling, LIU Wei. Maximum Likelihood-based Method for Locating Source of Negative Influence Spreading Under Independent Cascade Model [J]. Computer Science, 2022, 49(2): 204-215.
[11] SHEN Biao, SHEN Li-wei, LI Yi. Dynamic Task Scheduling Method for Space Crowdsourcing [J]. Computer Science, 2022, 49(2): 231-240.
[12] REN Shou-peng, LI Jin, WANG Jing-ru, YUE Kun. Ensemble Regression Decision Trees-based lncRNA-disease Association Prediction [J]. Computer Science, 2022, 49(2): 265-271.
[13] WANG Ze-qing, JI Sheng-peng, LI Xin, ZHAO Zi-xuan, WANG Peng-xu, HAN Xiao-song. Novel College Entrance Filling Recommendation Algorithm Based on Score Line Prediction andMulti-feature Fusion [J]. Computer Science, 2022, 49(11A): 211100266-7.
[14] ZHANG Bing-qing, FEI Qi, WANG Yi-chen, Yang Zhao. Study on Integration Test Order Generation Algorithm for SOA [J]. Computer Science, 2022, 49(11): 24-29.
[15] LI Kang-le, REN Zhi-lei, ZHOU Zhi-de, JIANG He. Decision Tree Algorithm-based API Misuse Detection [J]. Computer Science, 2022, 49(11): 30-38.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.