王立杰，劉昌祿，俞烈彬

(江蘇自動(dòng)化研究所，江蘇 連云港 222006)

嵌入式系統(tǒng)是一種嵌入到具體設(shè)備中，對(duì)性能、成本、功耗等有嚴(yán)格要求的專用計(jì)算機(jī)系統(tǒng)，目前已經(jīng)廣泛應(yīng)用于軍事、通訊、醫(yī)療、交通等行業(yè)中。運(yùn)行時(shí)系統(tǒng)功能的失效或者違反安全性、可靠性、實(shí)時(shí)性等非功能屬性都將導(dǎo)致災(zāi)難性的后果［1］。因此，提高軟件可信性成為嵌入式軟件開發(fā)領(lǐng)域的重要課題。

MARTE(Modeling and Analysis of Real Time and Embedded systems)是UML在嵌入式實(shí)時(shí)系統(tǒng)領(lǐng)域的建模規(guī)范［2］，彌補(bǔ)了UML對(duì)嵌入式實(shí)時(shí)領(lǐng)域的非功能屬性的表達(dá)能力的不足。UML/MARTE規(guī)范采用圖形化的方式描述系統(tǒng)，缺乏精確的語(yǔ)義信息，因此難以直接進(jìn)行一致性驗(yàn)證。形式化方法提供了一種嚴(yán)格精確的數(shù)學(xué)方法，通常被用于軟件設(shè)計(jì)階段，分析系統(tǒng)的可靠性［3］。Ahmed M.Mostafa等提出使用Z形式化UML用例圖、類圖、狀態(tài)圖等［4］。張?zhí)斓壤肁MMA平臺(tái)，在元模型層定義了MARTE到FIACRE的映射關(guān)系，完成了異構(gòu)轉(zhuǎn)換［5］。Soon-Kyeong Kim and David Carrington提出了元建模方法完成從UML圖到Object-Z的轉(zhuǎn)換，兩種語(yǔ)言定義在元模型層次，保證了轉(zhuǎn)換的精確性，完整性和一致性［6］。目前研究者對(duì)UML的形式化進(jìn)行了多方面的研究，并考慮MARTE與嵌入式系統(tǒng)的其它建模語(yǔ)言進(jìn)行轉(zhuǎn)換或集成，但對(duì)于MARTE模型的形式化基礎(chǔ)研究的還比較少。

本文首先建立了擴(kuò)展的Object-Z的元模型，以方便描述嵌入式時(shí)間和資源非功能屬性。然后在MDA框架下分別定義MARTE靜態(tài)結(jié)構(gòu)圖，動(dòng)態(tài)行為圖和時(shí)間資源非功能屬性到Object-Z語(yǔ)義的轉(zhuǎn)換規(guī)則，實(shí)現(xiàn)MARTE模型到Object-Z規(guī)約之間的轉(zhuǎn)換。從而可以根據(jù)Object-Z規(guī)范及其推理技術(shù)對(duì)MARTE模型進(jìn)行形式化的驗(yàn)證。由于轉(zhuǎn)換規(guī)則定義在元模型層，轉(zhuǎn)換規(guī)則可以重用。最后，將本文的轉(zhuǎn)換方法應(yīng)用到一個(gè)具體的案例，實(shí)現(xiàn)了兩個(gè)模型之間的轉(zhuǎn)換，驗(yàn)證了轉(zhuǎn)換方法的有效性。

1 基于MDA的模型轉(zhuǎn)換框架

MDA是一種以模型為中心的軟件開發(fā)框架［7］，其核心是模型和模型轉(zhuǎn)換，模型之間的轉(zhuǎn)換規(guī)則定義在元模型層?；贛DA的模型轉(zhuǎn)換解決了傳統(tǒng)模型轉(zhuǎn)換規(guī)則復(fù)雜而且難以重用的問(wèn)題［8］。

1.1 本文的模型轉(zhuǎn)換框架

在MDA的元-元模型體系中，UML/MARTE模型和Object-Z形式化描述屬于模型層(M1層)，而Object-Z模型的定義即Object-Z元模型和MARTE模型的元模型屬于元模型層(M2層)。MOF元對(duì)象設(shè)施為元-元模型的根(M3層)。本文首先建立遵從MOF元對(duì)象設(shè)施的擴(kuò)展的 Object-Z元模型，即將 Object-Z元模型和MARTE元模型納入到同一體系里，保證了轉(zhuǎn)換過(guò)程的同構(gòu);然后在元模型層定義映射關(guān)系;最后在模型層應(yīng)用轉(zhuǎn)換規(guī)則，實(shí)現(xiàn)轉(zhuǎn)換過(guò)程。如圖1所示。

圖1 MARTE模型和Object-Z模型之間的轉(zhuǎn)換

1.2 擴(kuò)展的Object-Z元模型

Z語(yǔ)言是一種形式化規(guī)格說(shuō)明語(yǔ)言，它以一階謂詞邏輯和集合論為基礎(chǔ)，支持表示抽象和操作抽象。Object-Z是Z的面向?qū)ο蟮臄U(kuò)展，可以方便地描述繼承、多態(tài)、關(guān)聯(lián)、聚集、組合等面向?qū)ο筇攸c(diǎn)。Object-Z規(guī)格說(shuō)明由類組成，類由狀態(tài)及定義在狀態(tài)上的操作組成。一個(gè)完整的Object-Z類模式如圖2所示。詳細(xì)的Object-Z語(yǔ)義參見文獻(xiàn)［9］。

圖2 Object-Z類模式

圖3是用類圖表示的Object-Z的核心元素元模型的結(jié)構(gòu)圖［8］。一個(gè)完整的Object-Z規(guī)約OZSpecification由 OZClass、OZOperation、OZAttribute 和 OZParameter、OZType等基本元素組成。其中本文添加了OZExpression和OZTimer兩種實(shí)時(shí)相關(guān)元素。OZExpression表示動(dòng)作執(zhí)行的約束條件，在Object-Z規(guī)約中為謂詞表達(dá)式。OZTimer為時(shí)間事件觀察器，表征行為的執(zhí)行時(shí)間相關(guān)因素。

圖3 一個(gè)擴(kuò)展的Object-Z元模型結(jié)構(gòu)圖

2 元模型層的映射規(guī)則

本文關(guān)注實(shí)時(shí)嵌入式系統(tǒng)模型的靜態(tài)結(jié)構(gòu)，動(dòng)態(tài)行為，時(shí)間和能量約束三個(gè)部分，分別用MARTE實(shí)時(shí)系統(tǒng)建模元素描述系統(tǒng)靜態(tài)結(jié)構(gòu)，狀態(tài)圖描述系統(tǒng)動(dòng)態(tài)行為，MARTE Profile標(biāo)記動(dòng)作執(zhí)行時(shí)間和能量約束。

2.1 靜態(tài)結(jié)構(gòu)到Object-Z的映射

靜態(tài)視圖展示系統(tǒng)里的事物的特征及它們之間的靜態(tài)聯(lián)系的總體模型的視圖。組成靜態(tài)視圖的最上層包括類元、聯(lián)系等。

2.1.1 MARTE 數(shù)據(jù)類型轉(zhuǎn)換

MARTE中使用的數(shù)據(jù)類型主要在MARTE模型庫(kù)(MARTE model library)中定義，MARTE中的基本數(shù)據(jù)類型 Integer，Unlimited Natural，Boolean 分別對(duì)應(yīng) Object-Z基本數(shù)據(jù)類型為Z，N，B三種類型。表1給出了從一些MARTE非基本數(shù)據(jù)類型到Object-Z類型之間的映射。其中與實(shí)時(shí)特征相關(guān)的數(shù)據(jù)類型有NFP-Duration，NFP-DateTime，NFP-Energy。

表1 MARTE數(shù)據(jù)類型到Object-Z類型的映射

2.1.2 MARTE 實(shí)時(shí)建模元素轉(zhuǎn)換

MARTE中設(shè)計(jì)模型主要封裝在高層應(yīng)用建模包HLAM中。如圖4所示，RtUnit和PpUnit表示實(shí)時(shí)嵌入式系統(tǒng)的活動(dòng)對(duì)象。

圖4 MARTE實(shí)時(shí)系統(tǒng)建模元素

實(shí)時(shí)特征可以直接通過(guò)RtUnit，PpUnit，RtService以及RtAction的屬性進(jìn)行建模。更加細(xì)致的實(shí)時(shí)建?？梢允褂肦ealTimeFeature構(gòu)造型。

根據(jù)實(shí)時(shí)建模元素的語(yǔ)義，定義表2中的映射。

2.2 動(dòng)態(tài)行為元素到Object-Z的映射

狀態(tài)圖表示有限狀態(tài)系統(tǒng)對(duì)外部事件響應(yīng)所形成的狀態(tài)遷移和動(dòng)作響應(yīng)。圖5給出了狀態(tài)機(jī)元模型。

圖5 狀態(tài)圖元模型

表2 MARTE靜態(tài)結(jié)構(gòu)到Object-Z之間的映射

根據(jù)UML狀態(tài)機(jī)元素的語(yǔ)義，定義表的映射如表3所示。

表3 狀態(tài)機(jī)元素與Object-Z語(yǔ)義的映射

2.3 時(shí)間和資源非功能屬性映射

本文關(guān)注行為的時(shí)間和能量約束兩方面的非功能屬性。構(gòu)造型?ResourceUsage?可以被用來(lái)定量地描述這兩方面的屬性。?ResourceUsage?的部分關(guān)系如圖6所示。UsageTypeAmount利用標(biāo)簽值(Tagged value)“execTime”標(biāo)記時(shí)間消耗，類型為NFP-Duration。利用“energy”標(biāo)記資源使用的數(shù)量，它的類型為NFPEnergy。在實(shí)時(shí)系統(tǒng)中，它表示單位時(shí)間內(nèi)的能耗量，而總能耗量則是單位時(shí)間能耗和執(zhí)行時(shí)間的乘積。

ResourceUsage標(biāo)記了行為執(zhí)行所消耗的時(shí)間和能量，具有時(shí)間和能量?jī)煞N狀態(tài)變化的行為模式，與OZClass語(yǔ)義相似，故將其映射為OZClass，其中執(zhí)行時(shí)間和能量的類型按此前定義的轉(zhuǎn)換規(guī)則映射為整數(shù)類型。如圖7所示。

圖6 ResourceUsage構(gòu)造型

圖7 ResourceUsage類模式

Object-Z在實(shí)時(shí)系統(tǒng)領(lǐng)域表達(dá)能力不足，沒有時(shí)間描述機(jī)制，難以滿足嵌入式模型對(duì)時(shí)間的要求。在Object-Z中定義定時(shí)器Timer和計(jì)時(shí)器DurationTimer兩種模式，分別表示系統(tǒng)當(dāng)前時(shí)間和時(shí)間間隔。Timer及其Object-Z表達(dá)如圖8所示。這種定義方式能滿足對(duì)嵌入式系統(tǒng)時(shí)間的要求，同時(shí)避免對(duì)Object-Z原語(yǔ)義進(jìn)行擴(kuò)充。

圖8 Timer及其Object-Z模式

在狀態(tài)圖中，能量消耗發(fā)生在狀態(tài)遷移中，如圖9所示。本文將ResourceUsage映射為對(duì)象類的一個(gè)操作模式，并且有如下定義:

TransitionResourceUsage?Transition∧ResourceUsage∧DurationTimer

3 模型轉(zhuǎn)換的實(shí)現(xiàn)

結(jié)合上文的映射規(guī)則，給出了一個(gè)具體實(shí)例——飛機(jī)著陸問(wèn)題，具體說(shuō)明轉(zhuǎn)換規(guī)則的應(yīng)用。

圖9 帶MARTE標(biāo)記的狀態(tài)圖

3.1 問(wèn)題描述

飛機(jī)著陸問(wèn)題(Aircraft Landing)描述了飛機(jī)著陸場(chǎng)景:飛機(jī)跑道每次僅容一架飛機(jī)降落，每架飛機(jī)都有一個(gè)目標(biāo)著陸時(shí)間(Target Time)和實(shí)際到達(dá)時(shí)間(Reach Time)。早到或晚到就有可能影響其它飛機(jī)的著陸。若沒有飛機(jī)處于等待狀態(tài)且跑道處于空閑狀態(tài)，則飛機(jī)直接著陸，否則系統(tǒng)通知其在空中徘徊等待先到的飛機(jī)著陸，因而消耗更多的燃料。處于等待狀態(tài)的飛機(jī)最多為2架，否則認(rèn)為不安全。如果所有處于等待狀態(tài)的飛機(jī)燃料充足，則系統(tǒng)按照飛機(jī)實(shí)際到達(dá)時(shí)間發(fā)送著陸通知，否則燃料不足的飛機(jī)先得到通知。所有得到著陸通知的飛機(jī)必須在10min內(nèi)著陸，并且在5min內(nèi)離開跑道。系統(tǒng)可以實(shí)時(shí)查詢飛機(jī)的狀態(tài)。

3.2 MARTE 建模

針對(duì)問(wèn)題中存在兩類實(shí)時(shí)單元Aircraft和Runway，結(jié)合MARTE實(shí)時(shí)系統(tǒng)建模元素和時(shí)間與資源建模元素，我們用 Aircraft類描述飛機(jī)的屬性和實(shí)時(shí)服務(wù)。Runway類則描述了飛機(jī)通知調(diào)度和查詢行為，目前MARTE 建模［10］已經(jīng)得到開源工具 Papyrus［10］的支持，如圖10、11、12系統(tǒng)模型圖。

靜態(tài)結(jié)構(gòu)圖中主實(shí)時(shí)單元Runway的生命周期等于系統(tǒng)的生命周期，它維護(hù)一個(gè)調(diào)度列表List，當(dāng)前狀態(tài)RunwayState。Runway根據(jù)與飛機(jī)的交互信息提供實(shí)時(shí)服務(wù):通知隊(duì)列中第一架飛機(jī)著陸start，飛機(jī)離開跑道后通知Runway執(zhí)行end。實(shí)時(shí)行為包含改變調(diào)度序列changeList，實(shí)時(shí)查詢飛機(jī)狀態(tài)query，更新調(diào)度列表sort。ExecutionKind是IocalImmediate，代表著得到交互信息后實(shí)時(shí)服務(wù)立即執(zhí)行。poolSize=2代表最多有兩架飛機(jī)等待降落。Aircraft類包含屬性飛機(jī)標(biāo)識(shí)id，最長(zhǎng)等待時(shí)間Time，當(dāng)前能量 Energy，當(dāng)前狀態(tài)AircraftState。Aircraft提供五種實(shí)時(shí)服務(wù)，飛機(jī)獲準(zhǔn)進(jìn)入機(jī)場(chǎng)空域appr，空中徘徊等待stop，飛機(jī)著陸land，直接著陸dirland，穿過(guò)跑道cross。其ExecutionKind都為deferred，表示該行為可延時(shí)執(zhí)行。concPolicy=reader聲明了同步策略，它表示同步發(fā)生沒有任何副作用。

圖10 Aircraft-Runway靜態(tài)結(jié)構(gòu)圖

圖11 帶MARTE標(biāo)記的Aircraft狀態(tài)圖

圖12 Runway狀態(tài)圖

在Aircraft的狀態(tài)圖中，ResourceUsage標(biāo)記了狀態(tài)遷移中行為的時(shí)間和能量消耗。作了如下假設(shè):1)Runway同意飛機(jī)進(jìn)入機(jī)場(chǎng)空域后，飛機(jī)轉(zhuǎn)換狀態(tài)的時(shí)間和能量消耗忽略不計(jì);2)飛機(jī)處于等待狀態(tài)時(shí)，單位時(shí)間消耗的能量是恒定的;3)飛機(jī)降落時(shí)必須將速度限制到一定范圍內(nèi)，著陸和穿過(guò)跑道時(shí)能量消耗存在一個(gè)上限。

3.3 模型轉(zhuǎn)換

根據(jù)上文中定義的轉(zhuǎn)換規(guī)則，將相應(yīng)的MARTE靜態(tài)圖、動(dòng)態(tài)圖和時(shí)間資源約束轉(zhuǎn)換為Object-Z描述。如圖13、14所示。限于篇幅，本文只詳細(xì)說(shuō)明Runway的sort操作模式。

圖13 Aircraft的Object-Z描述

Runway根據(jù)當(dāng)前的RunwayState和處于wait狀態(tài)的隊(duì)列長(zhǎng)度len進(jìn)行調(diào)度，如表4所示。根據(jù)以下條件，Runway可以通過(guò)操作sort的結(jié)果與飛機(jī)進(jìn)行實(shí)時(shí)交互，并更新調(diào)度列表。

表4 飛機(jī)調(diào)度條件

圖14 Runway的Object-Z描述

4 結(jié)束語(yǔ)

嵌入式軟件建模和形式化方法的結(jié)合可以大大提高嵌入式系統(tǒng)的可靠性。本文在模型驅(qū)動(dòng)的框架下，研究了嵌入式系統(tǒng)建模語(yǔ)言MARTE與形式化語(yǔ)言O(shè)bject-Z之間的轉(zhuǎn)換，主要做了如下工作:1)定義了基于MOF的實(shí)時(shí)擴(kuò)展Object-Z元模型;2)給出了MARTE模型和Object-Z的模型轉(zhuǎn)換框架;3)建立MARTE元模型和Object-Z元模型之間的可以重用的轉(zhuǎn)換規(guī)則。

嵌入式實(shí)時(shí)系統(tǒng)關(guān)注實(shí)時(shí)對(duì)象之間的通信，所以將序列圖的轉(zhuǎn)化為形式化模型是我們下一步的工作。同時(shí)由于本文只關(guān)注了嵌入式模型的時(shí)間和資源非功能屬性，下一步將在此基礎(chǔ)上分析MARTE其它非功能屬性建模元素如性能分析、吞吐量等。

［1］楊年華.模型驅(qū)動(dòng)架構(gòu)中的可信嵌入式軟件建模與分析［D］.上海:華東理工大學(xué)博士論文，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］張?zhí)?，JOUAULT，等.基于MDE的異構(gòu)模型轉(zhuǎn)換:從MARTE模型到 FIACRE模型［J］.軟件學(xué)報(bào)，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］劉亞萍，等.基于元建模的實(shí)時(shí)系統(tǒng)模型轉(zhuǎn)換方法研究.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，F(xiàn)rédéric Thomas，Charles André，Sébastien Gérard，F(xiàn)ran?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.