AADL-based Modeling and TPN-based Verification of Reconfiguration in Integrated Modular Avionics

This paper seeks to model the Integrated Modular Avionics (IMA) using Architectural Analysis and Design Language (AADL). In particular, the mechanism to describe the dynamic reconfiguration of multimodal system is presented. By translating the AADL model into Time Petri Net (TPN), some real-time and logical properties (deadlock, reach ability, missed deadline) of reconfiguration could be checked. The analysis results could then be used to adjust the design of software at the early stage of system development and ensure that the reconfiguration of IMA meets the real-time constraints.