基于Z-AADL模型的形式化轉換

高 正，曹子寧

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

基于Z-AADL模型的形式化轉換

高 正，曹子寧

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

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

Z-AADL；ZIA；CT-ZIA；模型轉換

0 引 言

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

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

(2)對目標系統進行AADL建模，然后將這種模型直接轉換為另一種形式化模型。

Z語言是一種嚴格的形式化規范描述語言，可以對狀態及狀態轉換之間的數據約束等進行嚴格的形式化描述。因此文中提出在AADL的基礎上擴展Z，形成Z-AADL規范，從而可以在不考慮具體設計細節的情況下，從更高的抽象級別用Z-AADL刻畫AADL模型。

1 AADL的Z擴充

1.1 AADL簡介

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

1.2 Z語言簡介

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

1.3 AADL的Z擴充規則

AADL的完整語義的形式化非常龐大，因此考慮一個AADL的子集，包括Thread,connection,behavior annex,系統執行模式等。文中主要對AADL中的behavior annex進行Z語言擴充。其中，behavior annex包括狀態集合以及狀態的轉換集合。約定：R表示變量之間的約束關系，ψ表示狀態轉換時所要滿足的約束性質，Computation表示狀態轉換時執行的操作。狀態的Z模式描述如下：

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

狀態轉換的Z模式描述如下：

Output;SrcState,DstState:STATE|SrcState.xi

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

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

狀態轉換時的約束性質的Z模式描述如下：

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

狀態轉換時所進行的操作模式描述如下：

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

1.4 基于連續時間的ZIA(CT-ZIA)

1.4.1 CT-ZIA的定義

ZIA[8-9]可以刻畫系統的行為和狀態，但是它并不能刻畫系統在實時方面的性質；時間自動機[10]是用來刻畫實時系統的一種自動機模型。文中將連續時間ZIA與時間自動機相結合，形成一種針對嵌入式實時系統的能夠同時刻畫行為和狀態的形式規范CT-ZIA[11]。

其中：

(1)SP是狀態集合。

根據陪護在患者身邊時發生跌倒墜床時的狀態描述可以看出，搬運患者、陪護在身邊睡覺、患者床邊大小便后陪護未安置好患者等情況為主（見表3）。

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

(8)映射I：SP→C(X)為每個狀態賦一時間約束，此約束稱為節點不變量。

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

下面給出CT-ZIA所對應的一種時序邏輯及其語法和語義。

1.4.2RT-DCL時序邏輯

文獻[12]通過在時序操作符上增加一個下標用于約束時間的范圍，從而得到一種時序邏輯RT-DCL，用這種時序邏輯可以作為CT-ZIA規范所對應的時序邏輯。

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。

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

定義4:RT-DCL的語義。

如果由Z-AADL模型轉換后得到的CT-ZIA模型是帶有數據約束的，刻畫如下：

2 Z-AADL到CT-ZIA的轉換

2.1 Z-AADL模型的刻畫

下面將實時系統用Z-AADL規范刻畫為一個七元組T=，其中：

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

(2)NT表示系統中關于數據性質描述的集合。性質包括但不限于1.3節中的Guard等數據性質。

(3)PT表示系統中接口的集合，包括線程、進程等構件中的輸入輸出接口。

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

(5)AT表示系統中動作的集合，即1.3節Transition中擴充了的操作模式Computation等。

(6)TRT表示系統中狀態轉換的集合，即1.3節中Behaviorannex中的狀態轉換Transitions，即擴充了的狀態轉換模式Transition的集合。

2.2 Z-AADL到CT-ZIA的轉換規則

從Z-AADL到基于連續時間CT-ZIA模型的轉化規則如下:

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

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

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

(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中的一個時鐘變量，映射為CT-ZIA模型P中的一個時鐘變量xi∈X，[ci,cj]∈TB是Z-AADL模型T中的一個時鐘基，[ci,cj]→xi表示將時鐘基[ci,cj]∈TB映射為CT-ZIA模型P中對于xi的時鐘約束。

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

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

3 模型轉換實例

鍋爐裝置在發電廠、船舶等領域應用廣泛，文獻[14]中對一個蒸汽鍋爐控制系統進行了自動機建模,文中參考此模型，建立了一個簡化的蒸汽鍋爐模型，它包括溫度控制器、供熱系統以及壓力控制器，如圖1所示。其中，溫度是由溫度控制器控制，壓力由閥門自動控制，供熱系統會向壓力控制器發送壓力值。

圖1 鍋爐系統

圖2展示了系統中溫度和壓力的狀態轉換關系，用變量x和y分別表示溫度和壓力。x?表示供熱系統從溫度控制器接收一個輸入變量,y!表示供熱系統向壓力控制器發送一個輸出變量。假設初始溫度和壓力分別為20 °C和100Kpa，初始狀態為l0。當壓力大于等于700時狀態會跳轉到l1，并將壓力置為700，壓力導數置為30，此后的狀態跳轉與此類似。

圖2 狀態轉換關系

鍋爐系統中的壓力會隨著溫度自動變化，因此下面只給出溫度控制器的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;

根據1.3節中的Z擴充規則，對AADL模型中的狀態、操作以及狀態變遷等進行Z模式的擴充。以l0，a0以及通過a0所做的狀態變遷為例，分別給出Z模式描述如下，后面的情形與此類似。

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

其中，x?表示狀態l0時的溫度，y!表示狀態l0時的壓力。

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

其中，l0；l1表示狀態變遷時的前狀態與后狀態。

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

根據上述狀態轉換關系，可以刻畫鍋爐系統的Z-AADL模型，即2.1節中的七元組模型T=。

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

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

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

(6)TRT={(l0,a0,l1),(l1,a1,l2),(l2,a2,l3),(l3,a3,l0)}表示系統中的狀態轉換的集合。

根據2.2節的模型轉換規則，可將上述的Z-AADL模型轉換為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 結束語

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

在AADL的擴展和形式化模型轉換方面取得了一定的成果，但是轉換后的模型是基于連續時間的無窮狀態模型，因此需要將其轉換為有限的域自動機模型來驗證。未來的主要工作是研究基于連續時間的CT-ZIA如何轉換為有限的域自動機模型，從而實現模型檢測。

[1] 楊志斌，皮 磊,胡 凱,等.復雜嵌入式實時系統體系結構設計與分析語言:AADL[J].軟件學報，2010，21(5)：899-915.

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

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

[4] 王立杰,劉昌祿,俞烈彬.基于MDA的MARTE模型形式化轉換[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行為模型驗證方法研究[J].計算機科學,2012,39(2):159-161.

[7] 倪水妹.面向混成系統的ZIA形式化模型及其自動驗證方法研究[D].南京:南京航空航天大學，2014.

[8] 李廣元，唐稚松．帶有時鐘變量的線性時序邏輯與實時系統驗證[J]．軟件學報，2002，13(1):33-41．

[9] 狄楊思，曹子寧，王 輝．一種基于形式規范ZIA的自動驗證方法[C]//火力控制技術/航空電子系統綜合技術2011年學術年會.出版地不詳：出版者不詳，2011：113-120．

[10] 孫全勇.時間自動機及其應用研究[D].哈爾濱：哈爾濱工程大學，2007.

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

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

[13] 錢俊彥,趙嶺忠,古天龍.一種基于時間自動機的時鐘等價性優化方法[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

時間：2017-01-04

國家“973”重點基礎研究發展計劃項目(2014CB744900)

高 正(1991-)，男，碩士研究生，研究方向為形式化方法；曹子寧，博導，研究方向為形式化方法、人工智能。

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