基于UPPAAL的AADL行为模型验证方法研究

Research on Verification Method of AADL Behavior Model Based on UPPAAL

为了实现AADL(体系结构分析与设计语言)行为模型的分析验证,基于行为附件的文法结构以及行为描述方式,提出了AADL行为模型与UPPAAL下时间自动机模型之间的模型转换规则。在转换规则的基础上,设计和实现了自动转换的原型工具。最后以航天器控制系统中制导、导航与控制计算机从陀螺取数的AADL模型为例,经自动转换得到时间自动机模型,并在UPPAAL下仿真、验证其行为正确性,同时证明了模型转换的有效性。

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.