A Compositional Verification Method for AADL Models of Safety-Critical Software

被引：0
作者：
Zhang B.-L. [1 ]
Yang Z.-B. [1 ,2 ]
Zhou Y. [1 ]
Ma Y.-Y. [1 ]
Huang Z.-Q. [1 ,2 ]
Xue L. [3 ]
机构：
[1] College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing
[2] Key Laboratory of Software Development and Verification Technology Ministry of Industry and Information Technology for High Security Systems, Nanjing
[3] Shanghai Aerospace Electronic Technology Institute, Shanghai
来源：
Jisuanji Xuebao/Chinese Journal of Computers | 2020年 / 43卷 / 11期
基金：
中国国家自然科学基金;
关键词：
AADL; Compositional verification; Rocket launch control system; Safety-critical software; UPPAAL;
D O I：
10.11897/SP.J.1016.2020.02134
中图分类号：
学科分类号：
摘要：
The complexity of safety-critical software has been higher and higher with the development of requirement specification. Therefore, it is a serious challenge to verify whether these complex systems satisfy expected properties or not. According to the example of the rocket launch control subsystem, this paper proposes a combination of compositional verification and model checking to complete the verification and analysis of the system. First, Architecture Analysis and Design Language (AADL) is used to hierarchically construct the architecture model of the rocket launch control subsystem, and the component requirements of each level of the system are formalized by contract theory, and then the correctness of the system architecture is verified through compositional verification. Secondly, the functional behavior of the components in the model are verified based on UPPAAL to ensure the correctness of component behaviors; Finally, the AADL model verification prototype tool is implemented to support the compositional verification of AGREE-based architecture models and UPPAAL-based component functional behavior verification, the rocket launch control subsystem case is used to show the effectiveness and limitations of the proposed method are demonstrated. © 2020, Science Press. All right reserved.
引用
收藏
页码：2134 / 2151
页数：17
相关论文
共 31 条
  • [1] Martins L E G, Gorschek T., Requirements engineering for safety-critical systems:Overview and challenges, IEEE Software, 34, 4, pp. 49-57, (2017)
  • [2] Rierson L., Developing Safety-Critical Software: A Practical Guide for Aviation Software and DO-178C compliance, (2013)
  • [3] Franzago M, Ruscio D D, Malavolta I, Et al., Collaborative model-driven software engineering: A classification framework and a research map, IEEE Transactions on Software Engineering, 44, 12, pp. 1146-1175, (2018)
  • [4] Cobleigh J M, Giannakopoulou D, Pasareanu C, Et al., Learning assumptions for compositional verification//Tools and Algorithms for the Construction and Analysis of Systems, (2003)
  • [5] Cofer D, Gacek A, Backes J, Et al., A formal approach to constructing secure air vehicle software, Computer, 51, 11, pp. 14-23, (2018)
  • [6] Chen H, Wu N, Shao Z, Et al., Toward compositional verification of interruptible OS kernels and device drivers, Journal of Automated Reasoning, 51, 6, pp. 1-49, (2017)
  • [7] Yang Z B, Lei P I, Hu K, Et al., AADL: An architecture design and analysis language for complex embedded real-time systems, Journal of Software, 21, 5, pp. 899-915, (2010)
  • [8] Berthomieu B, Bodeveix J P, Chaudet C, Et al., Formal verification of AADL specifications in the TOPCASED environment, Proceedings of the International Conference on Reliable Software Technologies, pp. 207-221, (2018)
  • [9] Cofer D, Gacek A, Miller S, Et al., Compositional verification of architectural models, Lecture Notes in Computer Science, 7226, pp. 126-140, (2012)
  • [10] Backes J, Cofer D, Miller S, Et al., Requirements analysis of a quad-redundant flight control system, Computer Science, 9058, pp. 82-96, (2015)
1234