The Modeling And Verification Of Cyber Physical System Based On AADL

Cyber Physical System is the next-generation intelligent system that combines computing resources and physical resources through the organic and deep integration of computation,communication and control technologies.The architecture analysis and design language is based on component,and is the standards architecture description language of embedded real-time system.AADL is widely used in avionics and other security critical areas of system modeling and analysis.In this paper,we studied the modeling and verification of CPS based on AADL,and proposed a framework of formal modeling and verification for CPS.Firstly,based on the AADL model elements,the modeling process,the CPS system characteristics and modeling requirements,we summarizes the advantages of AADL on the modeling of CPS hardware and software architecture and the lack of formal description of the large number of data constraints and concurrency relations in CPS.We extended the AADL based on the formal specification language Z and the process calculus.The Z-scheme and the concurrency,uncertainty and action constraints operators are added to AADL,and an architecture modeling specification CPS-AADL that can formalize the behavior of CPS system is proposed.Secondly,for the AADL does not support model checking directly,then we proposes a formal specification of component interaction automata with data constraint on the basis of automata research and development,which supports data component constraints and supports interactive description of system components.And a combined and verification algorithm and the model transition rules from CPS-AADL model to Z-COIA formal specification are given.Thirdly,the temporal logic system CIA-CTL oriented to Z-COIA is proposed on the basis of classical temporal logic,and its concrete semantic definition and model checking algorithm are given,then the model checking and verification of CPS-AADL can be realized.The feasibility and validity of the proposed formal modeling and verification framework are expounded through a formal modeling and verification process of a typical avionics cyber physical system-flight guidance system.