基于MDA的MARTE模型形式化转换  

MDA-based Formal Transformation Method for MARTE Model

作　　者：王立杰[1] 刘昌禄[1] 俞烈彬[1] 

机构地区：[1]江苏自动化研究所,江苏连云港222006

出　　处：《指挥控制与仿真》2012年第6期128-133,共6页Command Control & Simulation

基　　金：总装备部"十二五"基金项目

摘　　要：非形式化/半形式化模型到形式化模型之间的转换是当前软件工程领域的研究热点。根据异构模型转换,提出了基于MDA的MARTE模型到Object-Z规约之间的转换方法。针对Object-Z在实时领域表达能力不足的问题,首先扩展Object-Z元模型;然后在MDA的元元模型体系下,定义了MARTE元模型和扩展的Object-Z元模型之间的转换规则。MARTE模型可以重用这些转换规则以实现到Object-Z形式化描述之间的转换,进而可以对模型进行形式化验证;最后通过一个实例使用该方法完成模型转换,具体说明了转换规则的应用。Transformation between non-formal/semi-formal model and formal model is a research hotspot in software engineering domain. This paper proposed a MDA-based transformation method between MARTE model and Object-Z description for heterogeneous model transformation,This paper first expanded the Objeet-Z metamodel due to the shortcoming of Objeck-Z in real-time domain. Secondly, This paper defined the transformation rules between MARTE meta-model and Object-Z metamodel Under the meta-meta model system of MDA, MARTE model can be transformed to Objeet-Z specification by reusing the transformation rules, then formal verification can be done for MARTE model. Lastly, a case was proposed to complete the transformation using this method, specifying the application of the transformation rules.

关 键 词：模型驱动 MARTE模型 Object-Z规约 元模型 模型转换 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论] E917[自动化与计算机技术—计算机科学与技术]