Consistency Verification Of The AADL Model With Time Constraints

With the development of embedded real-time system,the complexity of the system was more and more high.The system needed to modeled abstractly and verified.Since its introduction by the Society of Automotive Engineers(SAE)in 2004,the Architecture Analysis and Design Language(AADL)had been widely used in aviation,aerospace,automotive electronics and weapons and equipment,and other information fields.The problem of model inconsistency caused by large-scale,complex layout and multi-person collaborative modeling was studied in this paper.The concrete work is as follows:First,the static structure and dynamic behavior of the AADL model were studied,and proposed the definition of static structure consistency and dynamic behavior consistency because of the lack of AADL model of static structure and dynamic behavior of consistency.This paper proposed the conversion rules and conversion algorithms of the relevant components of the static structure of AADL model to Prolog.Considering the limitation in component interaction,the static consistency of AADL model,such as port type consistency,traffic flow consistency and data type consistency,was verified based on prolog.By analyzing the characteristics of the mode transition,a formal description of the system initial state,state transition function and triggering event based on Prolog was established,and the transformation rules and algorithms of the model dynamic behavior related components to Prolog were proposed.At last,the static structure and dynamic behavior consistency of the model were verified and repaired in the case of the control panel in the avionics system.Comparing with the related work,this method can fully verify the consistency of AADL model.Secondly,according to the lack of time constraints in AADL model,an end-to-end data flow time constraint consistency verification framework was proposed and also an end-to-end data flow time constraint consistency verification method based on Prolog was proposed.The end-to-end data flow calculation method based on Prolog was given from three angles of data-driven,synchronous sampling and asynchronous sampling of task processing delay.The definition of time consistency and time constraint strong consistency were given based on relative time division of time interval.The time constraint consistency verification rule was designed based on Prolog.Take the end-to-end data flow in the model control panel as an example for model consistency verification and repair.Finally,the comparison of time delay analysis showed that the end-to-end data flow delay analysis method based on Prolog has a more comprehensive analysis of the time constraints of the model.Finally,based on the OSATE modeling platform,the AADL model verification plug-in was designed.The static structure consistency,dynamic behavior consistency and time constraint consistency of AADL model were verified.The simulation results showed that the AADL model verification plug-in can meet the requirements of AADL model consistency verification.