高 正，曹子寧

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016)

基于Z-AADL模型的形式化轉(zhuǎn)換

高 正，曹子寧

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016)

結(jié)構(gòu)分析與設(shè)計(jì)語言(Architecture Analysis and Design Language,AADL)是針對(duì)嵌入式實(shí)時(shí)系統(tǒng)領(lǐng)域中的軟件開發(fā)復(fù)雜度問題而提出的一種基于模型驅(qū)動(dòng)開發(fā)的體系結(jié)構(gòu)建模語言，可用于設(shè)計(jì)和分析一些安全關(guān)鍵嵌入式實(shí)時(shí)系統(tǒng)的軟硬件體系結(jié)構(gòu)。但是AADL嚴(yán)格來說只是一種半形式化的建模語言，雖然也描述了模型中構(gòu)件的屬性，但是對(duì)模型的非功能屬性并沒有明確的形式化描述，因此對(duì)AADL系統(tǒng)模型的非功能屬性進(jìn)行形式化驗(yàn)證，對(duì)于保證系統(tǒng)的正確性和可靠性具有重要意義。針對(duì)AADL模型中對(duì)非功能屬性及數(shù)據(jù)性質(zhì)等描述的不足之處，將其與形式規(guī)格說明語言Z語言相結(jié)合，提出了一種新的描述能力更加強(qiáng)大的形式規(guī)范語言—Z-AADL，并且定義了將Z-AADL模型轉(zhuǎn)換為形式化模型—ZIA模型的轉(zhuǎn)換規(guī)則，以實(shí)現(xiàn)Z-AADL模型到ZIA形式化模型的轉(zhuǎn)換。并通過一個(gè)轉(zhuǎn)換實(shí)例進(jìn)行說明。

Z-AADL；ZIA；CT-ZIA；模型轉(zhuǎn)換

0 引 言

嵌入式實(shí)時(shí)系統(tǒng)在航空航天、汽車控制、機(jī)器人等安全關(guān)鍵系統(tǒng)領(lǐng)域得到愈來愈廣泛的應(yīng)用。但由于計(jì)算精度、實(shí)時(shí)響應(yīng)、資源限制等要求的提高，系統(tǒng)開始變得越來越復(fù)雜，因此采用更加嚴(yán)格和可靠的設(shè)計(jì)與實(shí)現(xiàn)規(guī)范可以實(shí)現(xiàn)具有高可靠性、高質(zhì)量的復(fù)雜嵌入式實(shí)時(shí)系統(tǒng)[1-2]。針對(duì)這一越來越緊迫的問題，2004年，美國汽車工程師協(xié)會(huì)(SAE)提出了嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計(jì)標(biāo)準(zhǔn)-AADL[3]。它以傳統(tǒng)的建模語言MetaH、UML[4]為基礎(chǔ)，能夠更加精確地設(shè)計(jì)與分析嵌入式實(shí)時(shí)系統(tǒng)的軟硬件體系結(jié)構(gòu)及功能屬性等。但是，AADL仍然存在一些問題，有待進(jìn)一步的研究與完善。AADL采用自動(dòng)機(jī)的形式對(duì)線程、進(jìn)程等構(gòu)件的執(zhí)行狀態(tài)和動(dòng)作進(jìn)行了語義描述，但這種語義并不是嚴(yán)格的形式化語義描述，而且對(duì)于狀態(tài)及狀態(tài)轉(zhuǎn)換之間的數(shù)據(jù)約束關(guān)系也沒有形式化語義描述，因此難以直接進(jìn)行一致性檢驗(yàn)。結(jié)合國內(nèi)外對(duì)AADL建模語言多年的研究現(xiàn)狀，現(xiàn)在對(duì)AADL形式語義的研究多采用形式化轉(zhuǎn)換的方式，主要包括兩種：

(1)用某種具有精確語義的形式化語言來定義AADL的語義，然后通過這種語義來進(jìn)行形式化的轉(zhuǎn)換；

(2)對(duì)目標(biāo)系統(tǒng)進(jìn)行AADL建模，然后將這種模型直接轉(zhuǎn)換為另一種形式化模型。

Z語言是一種嚴(yán)格的形式化規(guī)范描述語言，可以對(duì)狀態(tài)及狀態(tài)轉(zhuǎn)換之間的數(shù)據(jù)約束等進(jìn)行嚴(yán)格的形式化描述。因此文中提出在AADL的基礎(chǔ)上擴(kuò)展Z，形成Z-AADL規(guī)范，從而可以在不考慮具體設(shè)計(jì)細(xì)節(jié)的情況下，從更高的抽象級(jí)別用Z-AADL刻畫AADL模型。

1 AADL的Z擴(kuò)充

1.1 AADL簡介

AADL是一種功能十分強(qiáng)大的分析與設(shè)計(jì)語言，越來越廣泛地應(yīng)用于航空電子、飛行控制等航空航天領(lǐng)域的嵌入式實(shí)時(shí)系統(tǒng)的體系結(jié)構(gòu)設(shè)計(jì)與分析中。它主要包括三大類組件，即：軟件組件、執(zhí)行平臺(tái)組件、系統(tǒng)組件。并且，在系統(tǒng)的建模過程中，通過包來組織所定義的組件類型和組件實(shí)現(xiàn)等內(nèi)容，這是一種類似于高級(jí)開發(fā)語言的組織形式。其中，軟件組件主要包括進(jìn)程組件、線程組件、線程組組件、數(shù)據(jù)組件、子程序組件、子程序組組件等。軟件組件的主要功能是用來表示系統(tǒng)的進(jìn)程、線程組、線程等應(yīng)用程序所具有的任務(wù)架構(gòu)，可用于表示模型所屬的軟件體系組成部分，例如數(shù)據(jù)組件中的數(shù)據(jù)類型、程序中的可執(zhí)行代碼等。執(zhí)行平臺(tái)組件主要包括處理器組件、存儲(chǔ)器組件、總線組件、外設(shè)組件等，主要功能是對(duì)系統(tǒng)的軟硬件體系結(jié)構(gòu)分層次建模，通常表現(xiàn)為系統(tǒng)中相關(guān)線程的調(diào)度、接口與接口之間的通信、接口與外部系統(tǒng)的通信等。系統(tǒng)組件的主要功能是將所建模的系統(tǒng)中所擁有的所有組件組合起來，形成一種分層次的系統(tǒng)結(jié)構(gòu)。AADL建模語言通過構(gòu)件、連接等來刻畫系統(tǒng)的軟硬件體系結(jié)構(gòu)；通過特征、屬性等來刻畫系統(tǒng)的性質(zhì)；當(dāng)系統(tǒng)需要在不同的工作模式之間切換時(shí)，它也可以通過模式轉(zhuǎn)換來刻畫系統(tǒng)的運(yùn)行體系演變。體系結(jié)構(gòu)、執(zhí)行模型和行為描述構(gòu)成一個(gè)完整的AADL模型,因此AADL語義也涉及這3個(gè)方面。文中主要是對(duì)AADL中的Behavior Annex[5-6]語義進(jìn)行擴(kuò)充的形式化描述。

1.2 Z語言簡介

Z語言[7]是一種基于一階謂詞邏輯和集合論的形式規(guī)格說明語言，它采用了嚴(yán)格的數(shù)學(xué)理論，可以對(duì)系統(tǒng)的行為特征和狀態(tài)值進(jìn)行簡明、精確、無歧義且可證明的形式化描述。Z模式是Z語言的核心，它有兩種模式：狀態(tài)模式和操作模式。狀態(tài)模式定義目標(biāo)軟件系統(tǒng)某一部分的狀態(tài)空間及其約束特征；操作模式描述了系統(tǒng)某一部分的行為特征，它通過描述操作前該部分的狀態(tài)值和操作后該部分狀態(tài)值之間的關(guān)系來定義系統(tǒng)該部分的一種操作特征。為了簡單明確地描述狀態(tài)與操作模式，Z規(guī)范中采用下述方式來表示變量：輸入變量的最后一個(gè)字符后跟隨一個(gè)“?”，輸出變量的最后一個(gè)字符后跟隨一個(gè)“!”。前狀態(tài)變量就是通常的變量，對(duì)應(yīng)的后狀態(tài)變量是以撇號(hào)“’”作為右上標(biāo)修飾的變量。

1.3 AADL的Z擴(kuò)充規(guī)則

AADL的完整語義的形式化非常龐大，因此考慮一個(gè)AADL的子集，包括Thread,connection,behavior annex,系統(tǒng)執(zhí)行模式等。文中主要對(duì)AADL中的behavior annex進(jìn)行Z語言擴(kuò)充。其中，behavior annex包括狀態(tài)集合以及狀態(tài)的轉(zhuǎn)換集合。約定：R表示變量之間的約束關(guān)系，ψ表示狀態(tài)轉(zhuǎn)換時(shí)所要滿足的約束性質(zhì)，Computation表示狀態(tài)轉(zhuǎn)換時(shí)執(zhí)行的操作。狀態(tài)的Z模式描述如下：

Output|xi?∈Input∧yj!∈Output;xi,yj:xiRyj]

狀態(tài)轉(zhuǎn)換的Z模式描述如下：

Output;SrcState,DstState:STATE|SrcState.xi

SrcState.xi=DstState.yi;SrcState.xj=DstState

.yj;xi,xj∈Input;yi,yj∈Output;]

狀態(tài)轉(zhuǎn)換時(shí)的約束性質(zhì)的Z模式描述如下：

Output|xi?∈Input∧yj!∈Output;φ∈ψ]

狀態(tài)轉(zhuǎn)換時(shí)所進(jìn)行的操作模式描述如下：

yn!:Output|xi?∈Input∧yj!∈Output;φ∈ψ]

1.4 基于連續(xù)時(shí)間的ZIA(CT-ZIA)

1.4.1 CT-ZIA的定義

ZIA[8-9]可以刻畫系統(tǒng)的行為和狀態(tài)，但是它并不能刻畫系統(tǒng)在實(shí)時(shí)方面的性質(zhì)；時(shí)間自動(dòng)機(jī)[10]是用來刻畫實(shí)時(shí)系統(tǒng)的一種自動(dòng)機(jī)模型。文中將連續(xù)時(shí)間ZIA與時(shí)間自動(dòng)機(jī)相結(jié)合，形成一種針對(duì)嵌入式實(shí)時(shí)系統(tǒng)的能夠同時(shí)刻畫行為和狀態(tài)的形式規(guī)范CT-ZIA[11]。

其中：

(1)SP是狀態(tài)集合。

根據(jù)陪護(hù)在患者身邊時(shí)發(fā)生跌倒墜床時(shí)的狀態(tài)描述可以看出，搬運(yùn)患者、陪護(hù)在身邊睡覺、患者床邊大小便后陪護(hù)未安置好患者等情況為主（見表3）。

(7)X為時(shí)鐘變量的非負(fù)實(shí)數(shù)有限集合，C(X)為X上時(shí)鐘約束的集合，其語法定義如下：Φ::=xc|cx|φ1∧φ2。其中，x∈X，∈{<,≤}，c為非負(fù)有理數(shù)。

(8)映射I：SP→C(X)為每個(gè)狀態(tài)賦一時(shí)間約束，此約束稱為節(jié)點(diǎn)不變量。

(9)TP是狀態(tài)之間轉(zhuǎn)換關(guān)系的集合，TP?SP×AP×C(X)×2X×SP。如果(s,a,φ,λ,s′)∈TP，那么表示在滿足轉(zhuǎn)換約束條件φ的前提下，通過動(dòng)作a∈AP(s)，狀態(tài)s可以遷移到新的狀態(tài)s'，同時(shí)λ?X中的時(shí)鐘被重置為0。

下面給出CT-ZIA所對(duì)應(yīng)的一種時(shí)序邏輯及其語法和語義。

1.4.2RT-DCL時(shí)序邏輯

文獻(xiàn)[12]通過在時(shí)序操作符上增加一個(gè)下標(biāo)用于約束時(shí)間的范圍，從而得到一種時(shí)序邏輯RT-DCL，用這種時(shí)序邏輯可以作為CT-ZIA規(guī)范所對(duì)應(yīng)的時(shí)序邏輯。

RT-DCL的語法也就是邏輯合法公式，定義如下：

定義2：RT-DCL的邏輯合法公式。

(2)若有φ1,φ2∈RT-DCL，則有φ1∨φ2∈RT-DCL。

(3)若有φ1,φ2∈RT-DCL，則有φ1∧φ2∈RT-DCL。

(6)若有φ1,φ2∈RT-DCL，則有Eφ1U～cφ2∈RT-DCL。其中，{<,≤,=,>,≥},c∈N。

(7)若有φ1,φ2∈RT-DCL，則有Aφ1U～cφ2∈RT-DCL。其中，{<,≤,=,>,≥},c∈N。

下面給出計(jì)算路徑CT-ZIA上的定義。

定義4:RT-DCL的語義。

如果由Z-AADL模型轉(zhuǎn)換后得到的CT-ZIA模型是帶有數(shù)據(jù)約束的，刻畫如下：

2 Z-AADL到CT-ZIA的轉(zhuǎn)換

2.1 Z-AADL模型的刻畫

下面將實(shí)時(shí)系統(tǒng)用Z-AADL規(guī)范刻畫為一個(gè)七元組T=，其中：

(1)ST={si:i∈}表示系統(tǒng)中狀態(tài)的集合，即1.3節(jié)中Behaviorannex中的狀態(tài)States，即擴(kuò)充了的Z狀態(tài)模式的集合。

(2)NT表示系統(tǒng)中關(guān)于數(shù)據(jù)性質(zhì)描述的集合。性質(zhì)包括但不限于1.3節(jié)中的Guard等數(shù)據(jù)性質(zhì)。

(3)PT表示系統(tǒng)中接口的集合，包括線程、進(jìn)程等構(gòu)件中的輸入輸出接口。

(4)CT表示系統(tǒng)中時(shí)鐘變量的非負(fù)實(shí)數(shù)集合，狀態(tài)轉(zhuǎn)換時(shí)所要滿足的時(shí)鐘約束；TB為CT上的時(shí)鐘基，時(shí)鐘基是時(shí)鐘變量的有序可數(shù)集合：TB={[ci,cj]|ci

(5)AT表示系統(tǒng)中動(dòng)作的集合，即1.3節(jié)Transition中擴(kuò)充了的操作模式Computation等。

(6)TRT表示系統(tǒng)中狀態(tài)轉(zhuǎn)換的集合，即1.3節(jié)中Behaviorannex中的狀態(tài)轉(zhuǎn)換Transitions，即擴(kuò)充了的狀態(tài)轉(zhuǎn)換模式Transition的集合。

2.2 Z-AADL到CT-ZIA的轉(zhuǎn)換規(guī)則

從Z-AADL到基于連續(xù)時(shí)間CT-ZIA模型的轉(zhuǎn)化規(guī)則如下:

(1)SP={si:sTi∈ST,i∈}，其中si∈SP是CT-ZIA模型P中的狀態(tài)，sTi∈ST是Z-AADL模型T中的狀態(tài)。

(2)AP={ai:aj∈AT,aj→ai,i,j∈}，其中aj∈AT是Z-AADL模型T中的動(dòng)作，aj→ai表示將模型T中的每一個(gè)動(dòng)作aj，映射為模型CT-ZIA中的一個(gè)動(dòng)作ai，根據(jù)動(dòng)作執(zhí)行者的不同，將它們分別歸入內(nèi)部動(dòng)作、輸入動(dòng)作和輸出動(dòng)作集合中。

(3)VP={vi:pi∈PT,pi→vi,i∈}，pi→vi表示將Z-AADL模型T中的接口用到的變量vi根據(jù)變量的擁有者分別把它們歸入到輸入變量、輸出變量和中間變量的集合中。

(6)X={xi:ci∈CT,i∈},C(X)={cx:[ci,cj]∈TB，i,j∈，[ci,cj]→xi,xi∈X,i∈}。其中ci∈CT是Z-AADL模型T中的一個(gè)時(shí)鐘變量，映射為CT-ZIA模型P中的一個(gè)時(shí)鐘變量xi∈X，[ci,cj]∈TB是Z-AADL模型T中的一個(gè)時(shí)鐘基，[ci,cj]→xi表示將時(shí)鐘基[ci,cj]∈TB映射為CT-ZIA模型P中對(duì)于xi的時(shí)鐘約束。

(7)I={si|→[ci,cj]:si→xi,[ci,cj]→xi,si∈S,[ci,cj]∈TB}，其中si→xi表示將Z-AADL模型T中的時(shí)鐘基TB中的時(shí)鐘對(duì)[ci,cj]轉(zhuǎn)換為CT-ZIA模型P中狀態(tài)si上的時(shí)鐘約束。

在系統(tǒng)內(nèi)部狀態(tài)變遷過程中，CT-ZIA中的狀態(tài)轉(zhuǎn)換是嚴(yán)格按照所要轉(zhuǎn)換的擴(kuò)充了Z語言的AADL系統(tǒng)中的狀態(tài)轉(zhuǎn)換映射過來的，這樣也就保證了在轉(zhuǎn)換過程中，系統(tǒng)內(nèi)部行為的一致性；而關(guān)于對(duì)時(shí)鐘的刻畫[13]，通過把實(shí)時(shí)系統(tǒng)中的時(shí)鐘變量提取出來，CT-ZIA中的時(shí)鐘變量是根據(jù)實(shí)時(shí)系統(tǒng)中的時(shí)鐘變量以及時(shí)間事件來進(jìn)行時(shí)鐘不變量的描述，這就確保了實(shí)時(shí)性的一致性描述；對(duì)于數(shù)據(jù)的約束能力，因?yàn)閷?shí)時(shí)系統(tǒng)中非功能屬性可以映射到Z語言模型，而CT-ZIA就是把數(shù)據(jù)用Z模式來進(jìn)行約束，這樣在數(shù)據(jù)約束能力方面它們采用的是一樣的Z模式，所以從實(shí)時(shí)系統(tǒng)轉(zhuǎn)換到CT-ZIA之后，它的行為和性質(zhì)與轉(zhuǎn)換之前保持了一致性。文獻(xiàn)[13]對(duì)模型轉(zhuǎn)換的正確性進(jìn)行了歸納證明，文中的證明與此類似。

3 模型轉(zhuǎn)換實(shí)例

鍋爐裝置在發(fā)電廠、船舶等領(lǐng)域應(yīng)用廣泛，文獻(xiàn)[14]中對(duì)一個(gè)蒸汽鍋爐控制系統(tǒng)進(jìn)行了自動(dòng)機(jī)建模,文中參考此模型，建立了一個(gè)簡化的蒸汽鍋爐模型，它包括溫度控制器、供熱系統(tǒng)以及壓力控制器，如圖1所示。其中，溫度是由溫度控制器控制，壓力由閥門自動(dòng)控制，供熱系統(tǒng)會(huì)向壓力控制器發(fā)送壓力值。

圖1 鍋爐系統(tǒng)

圖2展示了系統(tǒng)中溫度和壓力的狀態(tài)轉(zhuǎn)換關(guān)系，用變量x和y分別表示溫度和壓力。x?表示供熱系統(tǒng)從溫度控制器接收一個(gè)輸入變量,y!表示供熱系統(tǒng)向壓力控制器發(fā)送一個(gè)輸出變量。假設(shè)初始溫度和壓力分別為20 °C和100Kpa，初始狀態(tài)為l0。當(dāng)壓力大于等于700時(shí)狀態(tài)會(huì)跳轉(zhuǎn)到l1，并將壓力置為700，壓力導(dǎo)數(shù)置為30，此后的狀態(tài)跳轉(zhuǎn)與此類似。

圖2 狀態(tài)轉(zhuǎn)換關(guān)系

鍋爐系統(tǒng)中的壓力會(huì)隨著溫度自動(dòng)變化，因此下面只給出溫度控制器的AADL建模描述：

Threadimplementationtemp.impl

Features

x:indataporttemperature;

y:outdataportpressure;

Properties

Dispatch_Protocol=>Periodic;

Period=>50ms;

Compute_Execution_Time=>15ms..15ms;

Deadline=>50ms;

annexbehavior_specification**

states

l0:initialcompletestate;

transitions

l0-[]→l1{a0(30ms);x':=20,y':=y'+10};

l1-[]→l2{a1(15ms);x':=dx'+10,y':=y'};

l2-[]→l3{a2(15ms);x':=x',y':=y'-10};

l3-[]→l0{a3(15ms);x':=x'-10,y':=y'};

** ;

endtemp.impl;

根據(jù)1.3節(jié)中的Z擴(kuò)充規(guī)則，對(duì)AADL模型中的狀態(tài)、操作以及狀態(tài)變遷等進(jìn)行Z模式的擴(kuò)充。以l0，a0以及通過a0所做的狀態(tài)變遷為例，分別給出Z模式描述如下，后面的情形與此類似。

l0[x?:N;y!:N|x?<1 000;y!≥20];

其中，x?表示狀態(tài)l0時(shí)的溫度，y!表示狀態(tài)l0時(shí)的壓力。

transition[x?:N;y!:N;l0;l1|x?<1 000∧y'!≤940;x?=20∧y'!≤1 000];

其中，l0；l1表示狀態(tài)變遷時(shí)的前狀態(tài)與后狀態(tài)。

a0[x?:N;y!:N|x?=700;x'?=30];

根據(jù)上述狀態(tài)轉(zhuǎn)換關(guān)系，可以刻畫鍋爐系統(tǒng)的Z-AADL模型，即2.1節(jié)中的七元組模型T=。

(1)ST={l0,l1,l2,l3}表示系統(tǒng)中狀態(tài)的集合；

(2)NT={?(y!≥700),(x?≥660∧y!≥820),(x?≥960∧y!≥1 000),(x?≥900∧y!≥900)}；

(4)CT=[0,75],TB為CT上的時(shí)鐘基， TB={[0,30]，[30,45]，[45,60]，[60,75]}；

(6)TRT={(l0,a0,l1),(l1,a1,l2),(l2,a2,l3),(l3,a3,l0)}表示系統(tǒng)中的狀態(tài)轉(zhuǎn)換的集合。

根據(jù)2.2節(jié)的模型轉(zhuǎn)換規(guī)則，可將上述的Z-AADL模型轉(zhuǎn)換為CT-ZIA模型：

(1)SP={l0,l1,l2,l3};

(3)AP={a0,a1,a2,a3};

(4)VP={x?;y!};

(7)TP={(l0,a0,l1),(l1,a1,l2),(l2,a2,l3),(l3，a3,l0)}。

4 結(jié)束語

文中對(duì)AADL建模語言進(jìn)行了Z語言擴(kuò)充，形成了新的規(guī)范Z-AADL，從而使其不僅保留了原來的描述能力，而且具備了形式化的描述狀態(tài)及狀態(tài)轉(zhuǎn)換之間的數(shù)據(jù)約束方面的能力，為轉(zhuǎn)換為CT-ZIA形式化模型打下了基礎(chǔ)；然后研究了Z-AADL模型與CT-ZIA模型之間的轉(zhuǎn)換，使得轉(zhuǎn)換后的模型可以采用形式化方法進(jìn)行分析與驗(yàn)證等。

在AADL的擴(kuò)展和形式化模型轉(zhuǎn)換方面取得了一定的成果，但是轉(zhuǎn)換后的模型是基于連續(xù)時(shí)間的無窮狀態(tài)模型，因此需要將其轉(zhuǎn)換為有限的域自動(dòng)機(jī)模型來驗(yàn)證。未來的主要工作是研究基于連續(xù)時(shí)間的CT-ZIA如何轉(zhuǎn)換為有限的域自動(dòng)機(jī)模型，從而實(shí)現(xiàn)模型檢測。

[1] 楊志斌，皮 磊,胡 凱,等.復(fù)雜嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)設(shè)計(jì)與分析語言:AADL[J].軟件學(xué)報(bào)，2010，21(5)：899-915.

[2] 禚百田，付秀敏，鄭永果，等.基于UML的嵌入式實(shí)時(shí)系統(tǒng)開發(fā)方法[J].信息技術(shù)與信息化,2010(1):56-59.

[3]SAEAerospace.SAEAS5506:ArchitectureAnalysisandDesignLanguage(AADL)[EB/OL].2004.http://www.aadl.info/aadl/currentsite/.

[4] 王立杰,劉昌祿,俞烈彬.基于MDA的MARTE模型形式化轉(zhuǎn)換[J].指揮控制與仿真,2012,34(6):128-133.

[5]SAEAerospace.SAEAS5506annex:behavior_specificationV1.6.[EB/OL].2006.http://www.aadl.info/aadl/documents/Behaviour_Annex1.6.pdf.

[6] 李振松，顧 斌.基于UPPAAL的AADL行為模型驗(yàn)證方法研究[J].計(jì)算機(jī)科學(xué),2012,39(2):159-161.

[7] 倪水妹.面向混成系統(tǒng)的ZIA形式化模型及其自動(dòng)驗(yàn)證方法研究[D].南京:南京航空航天大學(xué)，2014.

[8] 李廣元，唐稚松．帶有時(shí)鐘變量的線性時(shí)序邏輯與實(shí)時(shí)系統(tǒng)驗(yàn)證[J]．軟件學(xué)報(bào)，2002，13(1):33-41．

[9] 狄楊思，曹子寧，王 輝．一種基于形式規(guī)范ZIA的自動(dòng)驗(yàn)證方法[C]//火力控制技術(shù)/航空電子系統(tǒng)綜合技術(shù)2011年學(xué)術(shù)年會(huì).出版地不詳：出版者不詳，2011：113-120．

[10] 孫全勇.時(shí)間自動(dòng)機(jī)及其應(yīng)用研究[D].哈爾濱：哈爾濱工程大學(xué)，2007.

[11] 倪水妹，曹子寧，李心磊.帶數(shù)據(jù)約束實(shí)時(shí)系統(tǒng)的模型檢測[J].計(jì)算機(jī)科學(xué),2014,41(5):254-262.

[12]LinHuiming,ZhangWenhui.Modelchecking:theories,techniquesandapplications[J].ActaElectronicaSinica,2002,30(S1):1907-1912.

[13] 錢俊彥,趙嶺忠,古天龍.一種基于時(shí)間自動(dòng)機(jī)的時(shí)鐘等價(jià)性優(yōu)化方法[J].計(jì)算機(jī)工程，2005，31(18)：71-73.

[14]HenzingerTA,Wong-ToiH.UsingHyTechtosynthesizecontrolparametersforasteamboiler[M].Berlin:Springer,1996.

Formal Transformation Basedon Z-AADL Model

GAO Zheng，CAO Zi-ning

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

Architecture Analysis and Design Language (AADL) is a kind of system structure modeling language based on model driven development in view of the problem of software development complexity in the field of embedded real-time system,which can be used to design and analyze the software and hardware architecture of some security critical embedded systems.But AADL is a semi-formal modeling language seriously.Although it also describes the properties of the components,the non-functional properties of the model are not clearly defined.Therefore,the formal verification of the non-functional properties of the AADL system model is of great significance to guarantee the correctness and reliability of the system.Aiming at the shortage of non-functional and data property of AADL model,combining the AADL specification with the Z language,a new specification—Z-AADL is put forward.Then the transformation rules between Z-AADL and ZIA is given,which define that how the Z-AADL model can be transformed to the ZIA model.An example is given to illustrate the transformation.

Z-AADL;ZIA;CT-ZIA;model transformation

2015-12-03

2016-03-17

時(shí)間：2017-01-04

國家“973”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃項(xiàng)目(2014CB744900)

高 正(1991-)，男，碩士研究生，研究方向?yàn)樾问交椒?；曹子寧，博?dǎo)，研究方向?yàn)樾问交椒ā⑷斯ぶ悄堋?/p>

http://www.cnki.net/kcms/detail/61.1450.TP.20170104.1023.030.html

TP31

A

1673-629X(2017)03-0023-06

10.3969/j.issn.1673-629X.2017.03.005