基于构件交互自动机的AADL模型转换方法研究

Investigation on AADL Model Transformation Method Based on Component-interaction Automata

构件交互自动机(Component-Interaction Automata,Co-IA)是扩展了构件之间交互描述的自动机。体系结构分析设计语言(Architecture Analysis and Design Language,AADL)是一种基于构件的半形式化体系结构分析和设计语言,是嵌入式系统体系结构建模和设计的标准,但无法直接进行形式化模型的检测工作。为了形式化描述系统交互过程中产生的大量数据,更好地描述模型中的状态集合、状态变迁和数据约束的性质,在构件交互自动机研究和发展的基础上,提出了一种扩充的构件交互自动机,将形式化规格说明语言Z引入构件交互自动机Z-Co IA,描述模型中包含状态和状态变迁。为检测与验证所建立的模型,基于具体实例进行了由AADL模型向经扩充的构件交互自动机模型的转换。验证结果表明,所提出的方法推动了AADL的形式化进程。

Component-Interaction Automata （Co-IA） is a automata which has expanded the interaction between components. Architec- ture Analysis and Design Language （AADL） is a kind of component-based semi-formal architecture analysis and design language and is the modeling and design standard of embedded system architecture. But it cannot detect the formal model directly. In order to formally de- scribe the large amounts of data produced by the interaction in the system and the characteristics of state sets, state change, data constraints in the model ,the expended ColA has been proposed on the basis of research and development of ColA. And the formal specification lan- guage Z is introduced into the ColA,named Z-ColA,to describe the status and status changes in the model. So as to test and verify the model ,transformation from the AADL to ColA is carded out by a concrete example. The verification results show that the proposed meth- od promotes the AADL formal process.