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

李 勇，李揭陽，曹子寧

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

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

李 勇，李揭陽，曹子寧

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

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

體系結構分析設計語言；構件式系統；計算樹邏輯；Z語言；模型檢測

0 引 言

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

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

1 背景簡介

1.1AADL

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

1.2CTL

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

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

1.3Z語言

Z語言[9-11]是一種形式化的軟件規范說明語言，由牛津大學的Abrial提出的基于一階謂詞邏輯和集合論的規范，由于采用了嚴格的數學基礎理論，Z語言使用最多的領域是狀態空間和數據結構的描述以及整體轉換。Z語言中包含了模式結構，其描述形式有垂直和水平兩種。

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

2 CZ_AADL建模規范(狀態變遷和數據約束)

2.1語法擴充

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

運用annex1|annex2的建模形式對不同形式的狀態遷移的組合構件模塊進行準確的組合建模，增強模型的可靠性和完整性。

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

圖1 annex中的狀態遷移的抽象描述

圖2 annex中擴充CTL和Z語言的

狀態遷移的抽象描述

2.2語義解釋

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

用Z語言規范來擴充AADL后，就可以采用形式化方法驗證帶數據約束的AADL系統模型，再將這種半形式化的模型轉換為形式化模型后，很多模型檢測算法就可以拿來作為檢測的工具。

這樣擴充了AADL原有的行為附件中的狀態遷移以及Z語言規范，可以彌補其在時序上針對時間不確定性的狀態變遷和數據約束性質的描述。

3 飛行管理系統設計實例

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

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

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

圖3 飛行管理系統簡圖

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

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

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在建模過程中對線程，進程，行為附件及連接等進行了一定的語義描述，但對于模型中的狀態及狀態遷移的時序性質和數據約束性質的描述略顯不足。對于構件式系統的建模，涵蓋了不同設計人員對于不同模塊所采取的不同建模方式，并通過對AADL進行的CTL擴充，使得所建立的模型可更好地融合成為安全可靠的模型。此外，Z語言對于數據約束方面的擴充也使得模型更加完備。

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

4 結束語

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

[1] 曾紅衛,繆淮扣.構件式系統的建模與驗證[J].計算機科學與探索,2008,2(2):198-205.

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

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

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

[5] 孫 健,徐 敏.基于AADL的嵌入式系統可調度性驗證[J].計算機技術與發展,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] 繆淮扣.軟件形式規格說明語言-Z[M].北京：清華大學出版社,2012.

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

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

[15] 肖健宇,張德運,陳海詮,等.模型檢測與定理證明相結合開發并驗證高可信嵌入式軟件[J].吉林大學學報:工學版,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">網絡出版時間

時間：2017-07-19

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

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

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