一種形式化組合式建模方法的研究

李 勇，李揭陽，曹子寧

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

一種形式化組合式建模方法的研究

李 勇，李揭陽，曹子寧

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

構(gòu)件式系統(tǒng)是一種采用構(gòu)件組合技術(shù)實現(xiàn)的結(jié)構(gòu)系統(tǒng)，即在采用單個構(gòu)件封裝簡單的業(yè)務(wù)功能基礎(chǔ)上，通過集成多個構(gòu)件逐步構(gòu)造新的組合構(gòu)件來實現(xiàn)比較復(fù)雜的業(yè)務(wù)功能。在開發(fā)構(gòu)件式系統(tǒng)軟件的過程中，正確的子構(gòu)件模型組合方式才有可能構(gòu)建安全可靠的總構(gòu)件模型。計算樹邏輯(CTL)能較為準(zhǔn)確地描述狀態(tài)遷移的時序性質(zhì)，而擅長形式規(guī)格說明的Z語言在數(shù)據(jù)約束方面具有強大作用。因此，基于CTL和Z語言對體系結(jié)構(gòu)分析設(shè)計語言(AADL)進(jìn)行功能拓展，即可建立更為安全可靠的組合模型。為此，在分析研究AADL的建模元素和建模流程的基礎(chǔ)上，提出了計算樹邏輯CTL和Z語言對AADL行為附件進(jìn)行擴(kuò)充的思路與方法。該方法可有效保證構(gòu)建模型的合理性和有序性?；贑Z_AADL建模規(guī)范和飛行管理系統(tǒng)實例進(jìn)行了驗證實驗。實驗結(jié)果表明，CZ_AADL建模規(guī)范增強了AADL建模的靈活性和多樣性，也為采用不同建模方式的多模塊間的融合提供了可能。

體系結(jié)構(gòu)分析設(shè)計語言；構(gòu)件式系統(tǒng)；計算樹邏輯；Z語言；模型檢測

0 引 言

構(gòu)件式系統(tǒng)是由多個子構(gòu)件組成的一個綜合性系統(tǒng)[1]，在軟件開發(fā)領(lǐng)域有著重要而廣泛的應(yīng)用，典型的比如無線局域網(wǎng)、物流服務(wù)供應(yīng)鏈系統(tǒng)等。由于構(gòu)件的可重用性、可移植性以及面向服務(wù)的計算模式等新技術(shù)的發(fā)展，在復(fù)雜的軟件系統(tǒng)設(shè)計中采用構(gòu)件式設(shè)計方法，可以顯著提高系統(tǒng)開發(fā)效率。因此，構(gòu)件式軟件開發(fā)方法已成為一種主流技術(shù)[2-3]。但是，在構(gòu)件式系統(tǒng)軟件的開發(fā)過程中仍然有許多由組合而衍生的安全可靠性方面的問題需要注意，即如何正確組合子構(gòu)件模型使其安全可靠，成為學(xué)術(shù)界的熱點研究領(lǐng)域之一。

體系結(jié)構(gòu)分析設(shè)計語言(Architecture Analysis and Design Language，AADL)提供了一種標(biāo)準(zhǔn)而又足夠精確的方式，設(shè)計與分析系統(tǒng)的軟硬件體系結(jié)構(gòu)及功能與非功能性質(zhì)，采用單一模型支持多種分析的方式，將系統(tǒng)設(shè)計、分析、驗證、自動代碼生成等關(guān)鍵環(huán)節(jié)融合于統(tǒng)一框架之下[4-5]，但為了適應(yīng)不同的應(yīng)用需求,AADL語言本身還需要進(jìn)一步完善和擴(kuò)展。AADL語言擴(kuò)展及其語義的形式化目的是為了更好地支持系統(tǒng)體系結(jié)構(gòu)建模與分析。為了滿足對構(gòu)件式系統(tǒng)的建模需求，采用計算樹邏輯(CTL)[6]以及形式規(guī)約語言-Z語言對AADL的行為附件進(jìn)行擴(kuò)充，并提出了構(gòu)建安全可靠模型的思路與方法。其中，CTL是一種具有離散時間概念的基于命題邏輯的時序邏輯，是一種重要的分支時序邏輯；Z語言是一種基于一階謂詞邏輯和集合論的形式規(guī)格說明語言，它采用了嚴(yán)格的數(shù)學(xué)理論，可以產(chǎn)生簡明、精確、無歧義且可證明的規(guī)格說明。為證明所建立模型的有效性和可行性，基于飛行管理系統(tǒng)的具體實例進(jìn)行實驗驗證。

1 背景簡介

1.1AADL

AADL是由SAE(汽車工程師協(xié)會)在2004年首次提出的一個標(biāo)準(zhǔn)，是對嵌入式系統(tǒng)體系結(jié)構(gòu)的高水平設(shè)計和評估。對于復(fù)雜系統(tǒng)建模，AADL通過包進(jìn)行組織。AADL提供了3種建模方式：文本、XML以及圖形化。當(dāng)定義新的屬性不能滿足用戶需要時，AADL引入了附件的概念。它擁有獨立的語法和語義,但必須與AADL核心標(biāo)準(zhǔn)保持語義一致。如故障模型附件(error model annex)，支持構(gòu)件、連接的故障事件、故障概率等屬性建模;行為附件[7](behavior annex)增強了AADL對構(gòu)件實際功能行為的詳細(xì)描述能力。

1.2CTL

CTL是一種分支時序邏輯，使用一個樹狀結(jié)構(gòu)來表示其時間模型，在未來路徑上狀態(tài)的性質(zhì)是不確定的。CTL公式的時態(tài)操作符是成對的：一個是路徑算子，分為以下兩種：A表示沿著樹狀結(jié)構(gòu)的所有路徑，E表示至少沿著樹狀結(jié)構(gòu)的某一條路徑；另一個是時態(tài)算子，分為以下四種：X表示樹狀結(jié)構(gòu)中某一節(jié)點的下一個節(jié)點，即下一個狀態(tài)；F表示樹狀結(jié)構(gòu)的某一個節(jié)點的后面節(jié)點，即未來某個狀態(tài)；G表示樹狀結(jié)構(gòu)中的所有節(jié)點即所有狀態(tài)；U表示直到樹狀結(jié)構(gòu)中的某節(jié)點之前的節(jié)點即直到某個狀態(tài)。

在合法的CTL公式中，類似AG、EF這樣的符號對是二元成對出現(xiàn)的，X、F、G和U算子之前必須有A或E算子，否則就是不合法的。類似的，每個A或E后面也必須跟著X、F、G和U算子，否則也是不合法的。文獻(xiàn)[8]中對計算樹邏輯的語法和語義給出了詳細(xì)描述。

1.3Z語言

Z語言[9-11]是一種形式化的軟件規(guī)范說明語言，由牛津大學(xué)的Abrial提出的基于一階謂詞邏輯和集合論的規(guī)范，由于采用了嚴(yán)格的數(shù)學(xué)基礎(chǔ)理論，Z語言使用最多的領(lǐng)域是狀態(tài)空間和數(shù)據(jù)結(jié)構(gòu)的描述以及整體轉(zhuǎn)換。Z語言中包含了模式結(jié)構(gòu)，其描述形式有垂直和水平兩種。

為了簡單明確地描述系統(tǒng)的狀態(tài)與操作，Z規(guī)范對系統(tǒng)中存在的輸入、輸出、前狀態(tài)變量和后狀態(tài)變量等一系列變量的表達(dá)方式做出了一些約定：變量后加“?”表示的是輸入變量，變量后加“!”表示的是輸出變量。并且用了一個撇號“’”加在后狀態(tài)變量上，用于區(qū)別對應(yīng)的前狀態(tài)變量，僅僅通過三個常見的符號就表達(dá)了四種類型的變量，Z語言規(guī)范的表達(dá)簡明性可見一斑。一個經(jīng)典的可以指定狀態(tài)的改變模式在文獻(xiàn)[12]中給出了詳細(xì)的描述。

2 CZ_AADL建模規(guī)范(狀態(tài)變遷和數(shù)據(jù)約束)

2.1語法擴(kuò)充

由于AADL本身自帶的行為附件annex里通過事件和狀態(tài)來描述相應(yīng)的狀態(tài)遷移，但是這也只能在組件間建立順序執(zhí)行的邏輯信息交換和訪問，對于組件信息傳遞路徑上的時序性質(zhì)不能進(jìn)行描述，另外對于組件之間數(shù)據(jù)的約束性質(zhì)的描述能力略顯不足。故在此引進(jìn)CTL和Z語言對AADL的行為附件annex進(jìn)行擴(kuò)充，對未來路徑上要滿足的時序性質(zhì)和數(shù)據(jù)約束性質(zhì)進(jìn)行描述，如圖1和圖2所示。

運用annex1|annex2的建模形式對不同形式的狀態(tài)遷移的組合構(gòu)件模塊進(jìn)行準(zhǔn)確的組合建模，增強模型的可靠性和完整性。

annex1behavior_specificationstatesstate1:initialstate;state2:state_one----------------------------staten:final_stateeventsEvent1:errorevent;Event2:normalevent;--------------------------------Eventn:otherevent;transitions:t0:state1-[Event1]->state2->[Event2]->…->[Eventn]->staten;

圖1 annex中的狀態(tài)遷移的抽象描述

圖2 annex中擴(kuò)充CTL和Z語言的

狀態(tài)遷移的抽象描述

2.2語義解釋

AADL本身具有的行為附件中使用transitions來描述狀態(tài)遷移，由一個事件event觸發(fā)一個狀態(tài)的改變遷移到另一個狀態(tài)，但這樣的狀態(tài)遷移在時序上是要有明確步驟的，即在設(shè)計系統(tǒng)時需要明確系統(tǒng)內(nèi)部的每一步狀態(tài)變遷。對于某些大型構(gòu)件式系統(tǒng)開發(fā)初期的設(shè)計，由于系統(tǒng)內(nèi)部狀態(tài)的遷移方面的細(xì)節(jié)可能還沒有明確的設(shè)計要求，這樣的狀態(tài)遷移描述顯然不能很好地完成整體設(shè)計任務(wù)。AADL擴(kuò)充了CTL后可以彌補這一設(shè)計上的不足，能夠很好地描述組件在未來某個時刻所保持的狀態(tài)。EX表示在某個組件的下一個組件的狀態(tài)；AX表示在所有組件的下一個組件的狀態(tài)；EG表示存在一個組件，其之后路徑上的所有組件的狀態(tài)；AG表示對所有的組件，其之后路徑上所有組件的狀態(tài)；EF表示存在一個組件，其之后的路徑上存在一個組件的狀態(tài)；AF表示對所有的組件，其之后的路徑上存在一個組件的狀態(tài)；E[φ1Uφ2]表示存在一條路徑上的所有組件都滿足φ1狀態(tài)，直到φ2在組件上滿足；A[φ1Uφ2]表示所有路徑上的所有組件都滿足φ1狀態(tài)，直到φ2在組件上滿足。

用Z語言規(guī)范來擴(kuò)充AADL后，就可以采用形式化方法驗證帶數(shù)據(jù)約束的AADL系統(tǒng)模型，再將這種半形式化的模型轉(zhuǎn)換為形式化模型后，很多模型檢測算法就可以拿來作為檢測的工具。

這樣擴(kuò)充了AADL原有的行為附件中的狀態(tài)遷移以及Z語言規(guī)范，可以彌補其在時序上針對時間不確定性的狀態(tài)變遷和數(shù)據(jù)約束性質(zhì)的描述。

3 飛行管理系統(tǒng)設(shè)計實例

下面給出一個實例，利用上面給出的擴(kuò)充后的AADL建模規(guī)范來建模，并著重分析擴(kuò)充CTL和Z語言后的AADL對于組件之間狀態(tài)遷移的時序性質(zhì)和數(shù)據(jù)變量約束的描述能力。

飛行管理系統(tǒng)(Flight Management System，F(xiàn)MS)[13]是航空電子系統(tǒng)的重要組成部分，是飛機重要的子系統(tǒng)。通常飛行員要借助FMS來完成飛機的起飛到著陸過程中的所有操作,飛行過程中FMS也可以參與實現(xiàn)飛機的自動飛行任務(wù)。FMS集多項功能于一體，其主要功能有飛行路線規(guī)劃、性能優(yōu)化、綜合導(dǎo)航與制導(dǎo)和控制顯示。

圖3是FMS的簡化功能示意圖，包括三個線程：傳感器處理線程、導(dǎo)航處理線程以及導(dǎo)航顯示線程。

圖3 飛行管理系統(tǒng)簡圖

定義兩個變量h,v分別表示飛機飛行的高度(最大值為12 km)和時速(最大值為1 000 km/h)，它們在模塊線程切換過程中滿足相應(yīng)的數(shù)據(jù)約束，在飛機處于正常飛行狀態(tài)時滿足一定的時序性質(zhì)。傳感器處理線程將捕獲的飛機位置的數(shù)據(jù)轉(zhuǎn)換成導(dǎo)航處理線程能夠識別的數(shù)字?jǐn)?shù)據(jù)，然后導(dǎo)航處理線程根據(jù)飛機的不同高度相應(yīng)地調(diào)整飛機的飛行速度以及其他導(dǎo)航工作，導(dǎo)航顯示線程把從導(dǎo)航處理線程得到的數(shù)據(jù)顯示在顯示設(shè)備上。

下面給出FMS擴(kuò)充后的AADL模型并分析Z語言在模塊切換過程中數(shù)據(jù)約束的描述能力。

thread NavigationSensorProcessing

Features

h,v：in data port sensor;

x,y：out data port sensor;

Properties

Dispatch _Protocol=>Periodic;

Period=>50ms;

Compute_Execution_Time=>5 ms..15 ms;

end NavigationSensorProcessing;

thread GuidanceProcessing

Properties

Dispatch_Protocol=>Periodic;

Period=>50ms;

Compute_Execution_Time=>8 ms..30 ms;

end GuidanceProcessing;

thread HandleProcessing

Properties

Dispatch_Protocol=>Periodic ;

Compute_Execution_Time=>1 ms..1 ms;

Period=>50ms;

end HandleProcessing;

annex behavior_specification **

states

s0:initial state;

transitions

**;

annex behavior_specification **

CTL:

states

s0:initial state;

temporal property

**;

AADL在建模過程中對線程，進(jìn)程，行為附件及連接等進(jìn)行了一定的語義描述，但對于模型中的狀態(tài)及狀態(tài)遷移的時序性質(zhì)和數(shù)據(jù)約束性質(zhì)的描述略顯不足。對于構(gòu)件式系統(tǒng)的建模，涵蓋了不同設(shè)計人員對于不同模塊所采取的不同建模方式，并通過對AADL進(jìn)行的CTL擴(kuò)充，使得所建立的模型可更好地融合成為安全可靠的模型。此外，Z語言對于數(shù)據(jù)約束方面的擴(kuò)充也使得模型更加完備。

從上面的建模的行為附件部分對于速度和高度數(shù)據(jù)的約束遷移和限制，可以看出CTL可以很好地描述狀態(tài)遷移的時序性質(zhì)[14]，運用CZ_AADL建模規(guī)范建立的模型可以對組件之間保持的時序性質(zhì)和組件之間的數(shù)據(jù)約束有了準(zhǔn)確描述，對于系統(tǒng)模型的刻畫進(jìn)一步完整。后續(xù)研究可將模型檢測和定理證明這兩種驗證方式相結(jié)合[15]，運用組合式的形式化驗證方法去驗證構(gòu)件式系統(tǒng)的安全可靠性。

4 結(jié)束語

對于復(fù)雜大型系統(tǒng)的建模，系統(tǒng)模型中的狀態(tài)及狀態(tài)變遷的時序性質(zhì)和數(shù)據(jù)約束性質(zhì)的描述極為重要，關(guān)系著系統(tǒng)的整體安全可靠性。為此，結(jié)合AADL建模規(guī)范，提出了在AADL的行為附件里擴(kuò)充CTL和Z語言的方法，并基于CZ_AADL建模規(guī)范和飛行管理系統(tǒng)實例進(jìn)行了驗證實驗。實驗結(jié)果表明，經(jīng)擴(kuò)充后的AADL建模規(guī)范增強了AADL建模的靈活性和多樣性，保證了系統(tǒng)的安全可靠性。后續(xù)研究可在組合式建模的基礎(chǔ)上進(jìn)行組合式方法的形式化驗證，將形式化方法運用到系統(tǒng)開發(fā)的各階段，從而給出從建模到驗證的一套完整的形式化開發(fā)框架。

[1] 曾紅衛(wèi),繆淮扣.構(gòu)件式系統(tǒng)的建模與驗證[J].計算機科學(xué)與探索,2008,2(2):198-205.

[2] 楊芙清,梅 宏,李克勤.軟件復(fù)用與軟件構(gòu)件技術(shù)[J].電子學(xué)報,1999,27(2):68-75.

[3] 于 東,盧艷軍,楊建剛.面向控制器的實時組件技術(shù)研究[J].小型微型計算機系統(tǒng),2004,25(12):2152-2155.

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

[5] 孫 健,徐 敏.基于AADL的嵌入式系統(tǒng)可調(diào)度性驗證[J].計算機技術(shù)與發(fā)展,2016,26(3):23-26.

[6] Huth M, Ryan M. Logic in computer science:modeling and reasoning about systems[M].New York,USA:Cambridge University Press,2004.

[7] Yang Z,Hu K,Ma D,et al.Towards a formal semantics for the AADL behavior annex[C]//Design,automation & test in europe conference & exhibition.[s.l.]:IEEE,2009:1166-1171.

[8] 周 慧.計算樹邏輯特性模式研究[J].計算機工程,2009,35(23):68-70.

[9] Spivey J M.The Z notation[M].[s.l.]:[s.n.],1989.

[10] Potter B,Till D,Sinclair J.Introduction to formal specification and Z[M].Upper Saddle River,NJ,USA:Prentice Hall,2015.

[11] Woodcock J,Davies J.Using Z:specification,refinement,and proof[M].Upper Saddle River,NJ,USA:Prentice-Hall,1996.

[12] 繆淮扣.軟件形式規(guī)格說明語言-Z[M].北京：清華大學(xué)出版社,2012.

[13] 湯小明,蘇羅輝,宋科璞.飛行管理系統(tǒng)AADL建模與分析[J].計算機技術(shù)與發(fā)展,2010,20(3):191-194.

[14] 蘇開樂,駱翔宇,呂關(guān)鋒.符號化模型檢測CTL[J].計算機學(xué)報,2005,28(11):1798-1806.

[15] 肖健宇,張德運,陳海詮,等.模型檢測與定理證明相結(jié)合開發(fā)并驗證高可信嵌入式軟件[J].吉林大學(xué)學(xué)報:工學(xué)版,2005,35(5):531-536.

ResearchonaFormalModelingMethodofCombination

LI Yong，LI Jie-yang，CAO Zi-ning

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

Component-based system is a combination of some components,that is,through the integration of the single component which packages the simple business function to build a new composite component to achieve more complex business functions.Only the correct combination of the subcomponents modeling can make it possible to construct a safe and reliable total component model.Computation Tree Logic (CTL) can well describe the temporal property of the state transition and Z language plays a significant role in the data constraint description.After expended AADL with Z language and CTL,the components can be combined with a reliable model.Therefore,based on the analysis of AADL modeling elements and modeling processes,the idea and method to improve AADL behavior annex with the computation tree logic and Z language have been presented,which can effectively ensure the rationality and orderliness of the model.The experiments for verification have been performed with the CZ_AADL modeling specification and the flight management system,which show that the CZ_AADL modeling specification has enhanced the flexibility and diversity of AADL modeling and provided possibility for integration of multiple modules with different modeling methods.

AADL;component-based system;CTL;Z language;model checking

2016-10-30

2017-02-15 < class="emphasis_bold">網(wǎng)絡(luò)出版時間

時間：2017-07-19

國家“973”重點基礎(chǔ)研究發(fā)展計劃項目(2014CB744900);航空科學(xué)基金(20150652008)

李 勇(1990-)，男，碩士生，研究方向為形式化方法;曹子寧,教授,博士生導(dǎo)師，研究方向為形式化方法、人工智能。

http://kns.cnki.net/kcms/detail/61.1450.TP.20170719.1109.030.html

TP301

A

1673-629X(2017)11-0106-04

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