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

王立杰，刘昌禄，俞烈彬

(江苏自动化研究所，江苏 连云港 222006)

嵌入式系统是一种嵌入到具体设备中，对性能、成本、功耗等有严格要求的专用计算机系统，目前已经广泛应用于军事、通讯、医疗、交通等行业中。运行时系统功能的失效或者违反安全性、可靠性、实时性等非功能属性都将导致灾难性的后果［1］。因此，提高软件可信性成为嵌入式软件开发领域的重要课题。

MARTE(Modeling and Analysis of Real Time and Embedded systems)是UML在嵌入式实时系统领域的建模规范［2］，弥补了UML对嵌入式实时领域的非功能属性的表达能力的不足。UML/MARTE规范采用图形化的方式描述系统，缺乏精确的语义信息，因此难以直接进行一致性验证。形式化方法提供了一种严格精确的数学方法，通常被用于软件设计阶段，分析系统的可靠性［3］。Ahmed M.Mostafa等提出使用Z形式化UML用例图、类图、状态图等［4］。张天等利用AMMA平台，在元模型层定义了MARTE到FIACRE的映射关系，完成了异构转换［5］。Soon-Kyeong Kim and David Carrington提出了元建模方法完成从UML图到Object-Z的转换，两种语言定义在元模型层次，保证了转换的精确性，完整性和一致性［6］。目前研究者对UML的形式化进行了多方面的研究，并考虑MARTE与嵌入式系统的其它建模语言进行转换或集成，但对于MARTE模型的形式化基础研究的还比较少。

本文首先建立了扩展的Object-Z的元模型，以方便描述嵌入式时间和资源非功能属性。然后在MDA框架下分别定义MARTE静态结构图，动态行为图和时间资源非功能属性到Object-Z语义的转换规则，实现MARTE模型到Object-Z规约之间的转换。从而可以根据Object-Z规范及其推理技术对MARTE模型进行形式化的验证。由于转换规则定义在元模型层，转换规则可以重用。最后，将本文的转换方法应用到一个具体的案例，实现了两个模型之间的转换，验证了转换方法的有效性。

1 基于MDA的模型转换框架

MDA是一种以模型为中心的软件开发框架［7］，其核心是模型和模型转换，模型之间的转换规则定义在元模型层。基于MDA的模型转换解决了传统模型转换规则复杂而且难以重用的问题［8］。

1.1 本文的模型转换框架

在MDA的元-元模型体系中，UML/MARTE模型和Object-Z形式化描述属于模型层(M1层)，而Object-Z模型的定义即Object-Z元模型和MARTE模型的元模型属于元模型层(M2层)。MOF元对象设施为元-元模型的根(M3层)。本文首先建立遵从MOF元对象设施的扩展的 Object-Z元模型，即将 Object-Z元模型和MARTE元模型纳入到同一体系里，保证了转换过程的同构;然后在元模型层定义映射关系;最后在模型层应用转换规则，实现转换过程。如图1所示。

图1 MARTE模型和Object-Z模型之间的转换

1.2 扩展的Object-Z元模型

Z语言是一种形式化规格说明语言，它以一阶谓词逻辑和集合论为基础，支持表示抽象和操作抽象。Object-Z是Z的面向对象的扩展，可以方便地描述继承、多态、关联、聚集、组合等面向对象特点。Object-Z规格说明由类组成，类由状态及定义在状态上的操作组成。一个完整的Object-Z类模式如图2所示。详细的Object-Z语义参见文献［9］。

图2 Object-Z类模式

图3是用类图表示的Object-Z的核心元素元模型的结构图［8］。一个完整的Object-Z规约OZSpecification由 OZClass、OZOperation、OZAttribute 和 OZParameter、OZType等基本元素组成。其中本文添加了OZExpression和OZTimer两种实时相关元素。OZExpression表示动作执行的约束条件，在Object-Z规约中为谓词表达式。OZTimer为时间事件观察器，表征行为的执行时间相关因素。

图3 一个扩展的Object-Z元模型结构图

2 元模型层的映射规则

本文关注实时嵌入式系统模型的静态结构，动态行为，时间和能量约束三个部分，分别用MARTE实时系统建模元素描述系统静态结构，状态图描述系统动态行为，MARTE Profile标记动作执行时间和能量约束。

2.1 静态结构到Object-Z的映射

静态视图展示系统里的事物的特征及它们之间的静态联系的总体模型的视图。组成静态视图的最上层包括类元、联系等。

2.1.1 MARTE 数据类型转换

MARTE中使用的数据类型主要在MARTE模型库(MARTE model library)中定义，MARTE中的基本数据类型 Integer，Unlimited Natural，Boolean 分别对应 Object-Z基本数据类型为Z，N，B三种类型。表1给出了从一些MARTE非基本数据类型到Object-Z类型之间的映射。其中与实时特征相关的数据类型有NFP-Duration，NFP-DateTime，NFP-Energy。

表1 MARTE数据类型到Object-Z类型的映射

2.1.2 MARTE 实时建模元素转换

MARTE中设计模型主要封装在高层应用建模包HLAM中。如图4所示，RtUnit和PpUnit表示实时嵌入式系统的活动对象。

图4 MARTE实时系统建模元素

实时特征可以直接通过RtUnit，PpUnit，RtService以及RtAction的属性进行建模。更加细致的实时建模可以使用RealTimeFeature构造型。

根据实时建模元素的语义，定义表2中的映射。

2.2 动态行为元素到Object-Z的映射

状态图表示有限状态系统对外部事件响应所形成的状态迁移和动作响应。图5给出了状态机元模型。

图5 状态图元模型

表2 MARTE静态结构到Object-Z之间的映射

根据UML状态机元素的语义，定义表的映射如表3所示。

表3 状态机元素与Object-Z语义的映射

2.3 时间和资源非功能属性映射

本文关注行为的时间和能量约束两方面的非功能属性。构造型≪ResourceUsage≫可以被用来定量地描述这两方面的属性。≪ResourceUsage≫的部分关系如图6所示。UsageTypeAmount利用标签值(Tagged value)“execTime”标记时间消耗，类型为NFP-Duration。利用“energy”标记资源使用的数量，它的类型为NFPEnergy。在实时系统中，它表示单位时间内的能耗量，而总能耗量则是单位时间能耗和执行时间的乘积。

ResourceUsage标记了行为执行所消耗的时间和能量，具有时间和能量两种状态变化的行为模式，与OZClass语义相似，故将其映射为OZClass，其中执行时间和能量的类型按此前定义的转换规则映射为整数类型。如图7所示。

图6 ResourceUsage构造型

图7 ResourceUsage类模式

Object-Z在实时系统领域表达能力不足，没有时间描述机制，难以满足嵌入式模型对时间的要求。在Object-Z中定义定时器Timer和计时器DurationTimer两种模式，分别表示系统当前时间和时间间隔。Timer及其Object-Z表达如图8所示。这种定义方式能满足对嵌入式系统时间的要求，同时避免对Object-Z原语义进行扩充。

图8 Timer及其Object-Z模式

在状态图中，能量消耗发生在状态迁移中，如图9所示。本文将ResourceUsage映射为对象类的一个操作模式，并且有如下定义:

TransitionResourceUsage≙Transition∧ResourceUsage∧DurationTimer

3 模型转换的实现

结合上文的映射规则，给出了一个具体实例——飞机着陆问题，具体说明转换规则的应用。

图9 带MARTE标记的状态图

3.1 问题描述

飞机着陆问题(Aircraft Landing)描述了飞机着陆场景:飞机跑道每次仅容一架飞机降落，每架飞机都有一个目标着陆时间(Target Time)和实际到达时间(Reach Time)。早到或晚到就有可能影响其它飞机的着陆。若没有飞机处于等待状态且跑道处于空闲状态，则飞机直接着陆，否则系统通知其在空中徘徊等待先到的飞机着陆，因而消耗更多的燃料。处于等待状态的飞机最多为2架，否则认为不安全。如果所有处于等待状态的飞机燃料充足，则系统按照飞机实际到达时间发送着陆通知，否则燃料不足的飞机先得到通知。所有得到着陆通知的飞机必须在10min内着陆，并且在5min内离开跑道。系统可以实时查询飞机的状态。

3.2 MARTE 建模

针对问题中存在两类实时单元Aircraft和Runway，结合MARTE实时系统建模元素和时间与资源建模元素，我们用 Aircraft类描述飞机的属性和实时服务。Runway类则描述了飞机通知调度和查询行为，目前MARTE 建模［10］已经得到开源工具 Papyrus［10］的支持，如图10、11、12系统模型图。

静态结构图中主实时单元Runway的生命周期等于系统的生命周期，它维护一个调度列表List，当前状态RunwayState。Runway根据与飞机的交互信息提供实时服务:通知队列中第一架飞机着陆start，飞机离开跑道后通知Runway执行end。实时行为包含改变调度序列changeList，实时查询飞机状态query，更新调度列表sort。ExecutionKind是IocalImmediate，代表着得到交互信息后实时服务立即执行。poolSize=2代表最多有两架飞机等待降落。Aircraft类包含属性飞机标识id，最长等待时间Time，当前能量 Energy，当前状态AircraftState。Aircraft提供五种实时服务，飞机获准进入机场空域appr，空中徘徊等待stop，飞机着陆land，直接着陆dirland，穿过跑道cross。其ExecutionKind都为deferred，表示该行为可延时执行。concPolicy=reader声明了同步策略，它表示同步发生没有任何副作用。

图10 Aircraft-Runway静态结构图

图11 带MARTE标记的Aircraft状态图

图12 Runway状态图

在Aircraft的状态图中，ResourceUsage标记了状态迁移中行为的时间和能量消耗。作了如下假设:1)Runway同意飞机进入机场空域后，飞机转换状态的时间和能量消耗忽略不计;2)飞机处于等待状态时，单位时间消耗的能量是恒定的;3)飞机降落时必须将速度限制到一定范围内，着陆和穿过跑道时能量消耗存在一个上限。

3.3 模型转换

根据上文中定义的转换规则，将相应的MARTE静态图、动态图和时间资源约束转换为Object-Z描述。如图13、14所示。限于篇幅，本文只详细说明Runway的sort操作模式。

图13 Aircraft的Object-Z描述

Runway根据当前的RunwayState和处于wait状态的队列长度len进行调度，如表4所示。根据以下条件，Runway可以通过操作sort的结果与飞机进行实时交互，并更新调度列表。

表4 飞机调度条件

图14 Runway的Object-Z描述

4 结束语

嵌入式软件建模和形式化方法的结合可以大大提高嵌入式系统的可靠性。本文在模型驱动的框架下，研究了嵌入式系统建模语言MARTE与形式化语言Object-Z之间的转换，主要做了如下工作:1)定义了基于MOF的实时扩展Object-Z元模型;2)给出了MARTE模型和Object-Z的模型转换框架;3)建立MARTE元模型和Object-Z元模型之间的可以重用的转换规则。

嵌入式实时系统关注实时对象之间的通信，所以将序列图的转化为形式化模型是我们下一步的工作。同时由于本文只关注了嵌入式模型的时间和资源非功能属性，下一步将在此基础上分析MARTE其它非功能属性建模元素如性能分析、吞吐量等。

［1］杨年华.模型驱动架构中的可信嵌入式软件建模与分析［D］.上海:华东理工大学博士论文，2010.

［2］OMG.UML Profile for MARTE:Modeling and Analysis of Real-time Embedded Systems.2011.http:∥www.omg.org/spec/MARTE/1.1.

［3］Ermeson Andrade，Paulo Maciel，Gustavo Callou，Bruno Nogueira.Mapping UML Interaction Overview Diagram to Time Petri Net for Analysis and Verification of Embedded Real-Time SystemswithEnergyConstraints.CIMCA 2008，2008:615-620.

［4］M.Mostafa A，Ismail MA，EL-Bolok H et al.Toward a Formalization of uml2.0 Metamodel Using Specifications.In:8th ACIS International Conference on Software Engineering，Artificial Intelligence，Networking，and Parallel/Distributed Computing;SNPD，2007:694-701.

［5］张天，JOUAULT，等.基于MDE的异构模型转换:从MARTE模型到 FIACRE模型［J］.软件学报，2009，20(2):214-233.

［6］Kim S-K，Carrington D.A Formal Mapping between UML Models and Object-Z Specifications.In:LNCS 1878;2000:Springer-Verlag;2000:2-21.

［7］OMG.MDA Guide Version 1.0.1.2009.http∥www.omg.org/cgi-bin/doc?omg/03-06-01.

［8］刘亚萍，等.基于元建模的实时系统模型转换方法研究.Journal of Chinese Computer Systems，2010，31(11):2145-2153.

［9］Kim S-K，Carrington D.A Formal Metamodeling Approach to a Transformation Between the UML State Machine and object-Z.In:ICFEM 2002，LNCS 2495;2002;Springer-Verlag Berlin Heidelberg;2002:548-560.

［10］Sébastien Demathieu，Frédéric Thomas，Charles André，Sébastien Gérard，François Terrier.First experiments using the UML profile for MARTE.11th IEEE Symposium on Object Oriented Real-Time Distributed Computing(ISORC)，2008:50-57.

［11］CEA List Team.Papyrus1.12(open source tool for graphical UML2 modeling).http:∥www.papyrusuml.org，2008.