Real-time Verification Of The Embedded System Model Based On AADL Using UPPAAL

With the increasing size, complexity and reliability requirements of embedded system, thearchitecture development method of model driven has become popular in embedded real-time system.Architecture Analysis and Design Language (AADL) is a new standard of model driven systemengineering for embedded real-time system. It supports soft/hardware structural modeling, andimports non-functional attributes description such as real-time and security qualities. During theprocess of MDD (Model-Driven Development), it is of great significance for ensuring the systemreal-time performance and improving the efficiency of system development to find potential designproblems on critical aspects in the model design stage.In order to analyze the schedulability and flow latency of AADL models, time automata isestablished for both scheduling model and data flows of AADL model using the formal analysismethod, which realizes model transformation and verification. On building the scheduling modeltimed automata, scheduling policy based on AADL is analyzed. Periodic and aperiodic thread timedautomata templates, preemptive and non-preemptive scheduler timed automata templates are designedaccording to features and proprieties of AADL models. The mapping semantic between AADLscheduling model and timed automata model is given to guide the transformation from componentsand proprieties of AADL models to timed automata. On building the timed automata of date flows,methods and samples are given to transform both simple and mixed flows into timed automata. Thetimed automate based on the mixed flows communicates with the scheduling model timed automate,so that they are combined as a timed automate network and can be test and verified as a whole.In order to realize the automation of model transformation process, an Eclipse plug-in isdeveloped and integrated to the AADL modeling tool OSATE, so that the modeling, transformation,verification and analyzing methods can be realized in an integrated environment. Finally, the timedautomate model is simulated and verified in the tool UPPAAL to analysis whether the original AADLmodel meets the designed real-time qualities. Experimental results show that the modeltransformation method is valid and schedulability and flow latency qualities can be verifiedeffectively by this method.