导航

ACTA AERONAUTICAET ASTRONAUTICA SINICA ›› 2022, Vol. 43 ›› Issue (3): 325196-325196.doi: 10.7527/S1000-6893.2021.25196

Previous Articles     Next Articles

Formal verification technology for AADL models based on NuSMV

LIU Chang1, JIANG Yongping2, MA Chunyan2, ZHANG Tao2   

  1. 1. China Aeronautical Radio Electronics Research Institute, Shanghai 200233, China;
    2. School of Software, Northwestern Polytechnical University, Xi'an 710072, China
  • Received:2020-12-31 Revised:2021-01-27 Online:2022-03-15 Published:2021-03-09
  • Supported by:
    Aviation Science Foundation (20175553028, 20185853038, 201907053004)

Abstract: Architecture Analysis and Design Language (AADL) is a modeling language used to describe the architecture and behavior of mission critical embedded system, which is widely used in the aerospace field.To verify the correctness of the key attributes of AADL model and system behavior, this paper studies the formal verification method for the AADL model based on NuSMV(New Symbolic Model Verifier).Firstly, covering all the software components and behavior characteristics of AADL model, mapping rules and transformation algorithm from the AADL model to the NuSMV model are proposed.Secondly, correctness of the transformation algorithm is analyzed by the graph isomorphism method.Then, the temporal logic formula is used to describe the attributes to be verified in the NuSMV model, so as to verify the safety, activity and nested mode configuration in the AADL model.Finally, taking the flight control system as an example, the formal verification method of AADL model based on NuSMV is explained in detail, and the statistical information of verification attributes is given.

Key words: AADL model, NuSMV, formal verification, model transformation, flight control system

CLC Number: