Systems Engineering and Electronics ›› 2022, Vol. 44 ›› Issue (4): 1282-1290.doi: 10.12305/j.issn.1001-506X.2022.04.26

• Systems Engineering • Previous Articles     Next Articles

Simulation and verification of DIMA dynamic reconfiguration based on formal method

Jiachen LIU1,2, Lei DONG1,2,3,*, Changxiao ZHAO1,2,3, Hongbing CHEN1,2   

  1. 1. College of Safety Science and Engineering, Civil Aviation University of China, Tianjin 300300, China
    2. Key Laboratory of Civil Aircraft Airworthiness Technology, Civil Aviation University of China, Tianjin 300300, China
    3. Civil Aircraft Airworthiness and Repair Key Laboratory of Tianjin, Tianjin 300300, China
  • Received:2021-02-17 Online:2022-04-01 Published:2022-04-01
  • Contact: Lei DONG

Abstract:

In view of the lack of simulation and verification means in the early design stage of reconfigurable distributed integrated modular avionics (DIMA) system, the architecture characteristics of reconfigurable DIMA software system and the component function division of hierarchical generic system management (GSM) supporting dynamic reconfiguration are analyzed firstly. Then, architecture analysis and design language (AADL) and its related accessories are used to model the architectural basis, behavior details and other elements of DIMA dynamic reconfiguration. On this basis, a model transformation rule based on formal definition is designed, which transforms AADL dynamic reconstruction model into executable timed automata model. Finally, the correctness of logic and timing of reconfigurable DIMA system and the accessibility of unsafe control behavior are verified by using model verification tool UPPAAL. The results show that the proposed method is feasible and effective, and can provide a model basis for the formal security evaluation of subsequent DIMA dynamic reconfiguration.

Key words: distributed integrated modular avionics (DIMA), dynamic reconfiguration, architecture analysis and design language (AADL), formal method, simulation verification

CLC Number: 

[an error occurred while processing this directive]