基于MDA的MARTE模型形式化方法  

Formal method of MARTE model based on MDA

作　　者：许海洋[1] 王萍[1] 

机构地区：[1]青岛农业大学理学与信息科学学院,山东青岛266109

出　　处：《计算机应用研究》2012年第8期3018-3021,共4页Application Research of Computers

摘　　要：针对嵌入式系统对可靠性和可预测性的要求,提出基于MDA对嵌入式系统的建模语言MARTE进行形式化描述的方法。建立Object-Z的元模型,定义了MARTE元模型与Object-Z元模型之间的模型转换关系,给出了MARTE模型到Object-Z模型的语义映射和语法转换的具体过程。该方法支持将MARTE模型形式化转换为Object-Z模型,有利于软件开发早期的检验和验证。For the reliability and predictability requirements of embedded systems, this paper proposed MDA-based method to formal describe MARTE, which was a modeling language for embedded systems. It established Object-Z metamodel, and defined model transformation relationship between MARTE metamodel and Object-Z metamodel. It also presented the specific process of semantic mapping and the syntax conversion between MARTE model and Object-Z model. The method supported the formal translation between MARTE model and Object-Z model, it was helpful to test and verify in the early stage of the software development.

关 键 词：模型驱动体系 形式化方法 模型转换 MARTE元模型 

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