Research on Verification Method of AADL Behavior Model Based on UPPAAL
Bin Gu · 2012
To analyse and validate AADL(architecture analysis and design language) behavior model,a mapping regulation between AADL behavior model and timed automata model of UPPAAL was proposed based on the syntax definition of AADL behavior annex and the descriptive way of behavior.On the basis of the transformation rules,a prototype tool for automatic conversion was designed and implemented.Finally an AADL model of guidance navigation and control computer getting data from gyroscope in spacecraft control system was translated into a timed automata model using the tool,to simulate and verify its behavior using UPPAAL.The experiment demonstrates the validity of the model transformation.