Formal Modeling And Verification Of Avionics Systems

Architecture analysis and design language is a kind of architecture description language standard for embedded real-time system. It is widely used in aviation aerospace industry. To ensure the correctness and reliability of the AADL model has become a hot research field. AADL specification describe the semantics of the thread, process, the behavior annex, connection in model, but for the states and states with the data constraints description is slightly less than, and the formal specification language Z language in the data constraint description has a significant role. After expended AADL with Z language, the model can be better transformed to a formal model, which makes model checking technology can be used to convert the model. As a strict mathematical based verification technique, model checking can be used to accurately, abstract and concise specification and verification of software system and its properties, and to ensure the safety and reliability of the software.The paper converts Z-AADL model to formal model for verification to ensure the software reliability. First of all, we extend AADL specification by combining AADL with Z-language, and this new specification—Z-AADL can describe Real-time and Embedded systems with data constraints. Secondly, we put forward a formal specification which describes real-time system with data constraints?ZIA specification based on continuous-time, and convert Z-AADL model to ZIA model based on continuous-time. When we realize model checking for ZIA model based on continuous-time, we also realize model checking for Z-AADL model. Finally, we give the model checking algorithm of the ZIA specification based on continuous-time, and demonstrate the feasibility and effectiveness of the method in the article by verify the method with an example.Beside, the traditional ZIA did not characterize the probability aspect of the system.So we expand probabilistic nature on the traditional ZIA and present a probabilistic system specification?DT-PZIA,so that it can not only characterize the behavior and state of the system,but also characterize the probabilistic nature of the Compared with the traditional temporal logic,it not only save the ability to reflect the temporal properties, but also reflect the probability nature of the system. Then we also give a model checking algorithm for performance queries of probabilistic systems.