《軟件架構理論與實踐》 —3.3　軟件架構的形式化建模方法

3.3　軟件架構的形式化建模方法

軟件架構建模通常采用非形式化方法，然而這種非形式化方法并不能很好地描述不同系統組成部分之間的一些特性，已經難以適應軟件架構建模的進一步發展。同時形式化方法作為一種嚴格以數學為基礎的方法，能夠清晰、精確、抽象、簡明地規范和驗證軟件系統及其性質，幫助發現其他方法不容易發現的系統描述的不一致、不明確或不完整，有助于增強軟件開發人員對系統的理解。總之，形式化的建模方法能夠極大地提高軟件的非功能屬性。

目前，在軟件架構建模中，包含基于形式化規格說明語言的建模和基于UML形式化的建模兩種軟件架構形式化建模方法[47]。

1）基于形式化規格說明語言的建模：其基本思想是利用一些已知特性的數學抽象來為目標軟件系統的狀態特征和行為特征構造模型，如Z語言、B語言、VDM、Petri網等都是面向模型的方法。或者，它為目標軟件系統的規格說明提供了一些特殊的機制，包括描述抽象概念并進行進程間連接和推理的方法，如CSP、CCS、CLEAR等都是代數方法。

2）基于UML形式化的建模：其基本思想是利用形式化與UML結合的建模方法研究成果，對UML圖形賦予形式化語義，然后就可以利用已有的形式化語言和工具對UML模型進行推理驗證。我們可以將UML相關圖形轉換成Z語言、B語言、XYZ/E、Petri網等不同的形式化語言，這提高了UML的準確性，為精確建模奠定了良好的基礎。

3.3.1　基于形式化規格說明語言的建模方法

軟件開發中的形式化建模方法主要是使用形式化規格說明語言來展示系統的架構，解析系統的特性。目前廣泛應用的一些形式化描述方法有Z語言、Petri網、B語言、VDM、CSP等，這些形式化方法在功能上各有側重，可以互補。

1. Z語言

Z語言是迄今為止應用最為廣泛的形式化語言之一，軟件企業在軟件特別是大型軟件的開發中經常采用Z語言進行需求分析、軟件架構建模。Z語言是由英國牛津大學程序研究組（PRG）的Jean Raymond Abrial、Bernard Sufrin等人設計的一種基于一階謂詞邏輯和集合論的形式化規格說明語言，它采用了嚴格的數學理論，將函數、映射、關系等數學方法用于規格說明，具有精確、簡潔、無二義性且可證明等優點。Z語言是一種功能很強的形式化規格說明語言，可以保證其書寫的規格說明文檔的正確性，同時還能保證有很好的可讀性和可理解性。Z語言借助于模式（schema）來表達系統結構。模式有水平和垂直兩種形式。一個模式由變量聲明和謂詞約束兩部分組成，可用來描述系統的狀態和操作，即“模式=聲明+謂詞”。聲明部分引入變量，謂詞部分表示了關于變量值的要求。

Z語言規范一般由四個部分組成：給定的集合、數據類型和常數；狀態定義；初始狀態；操作。在實際應用中，Z語言的一個規范（即語言文檔）由形式化的數學描述和非形式化的文字解釋或說明組成。形式化的數學描述由段落構成，這些段落按順序給出各種構造類型描述、全局變量定義以及基本類型描述。具體描述時，一個段落可以給出一個或多個構造類型描述。根據段落的含義不同，段落的種類有基本類型、公理、約束條件、構造類型、縮寫、通用構造類型、通用常量和自由類型。

Z語言作為一種廣泛應用的形式化規格說明語言，在軟件架構建模方面也得到了廣泛關注。通過使用Z語言對軟件架構進行形式化建模，軟件開發者可以得到精確、嚴謹的架構描述。文獻[48]中運用Z語言給出了管道–過濾器結構詳盡的形式化描述的實例。該結構包括過程抽象和操作抽象。其中，過程抽象包括管道模式、過濾器模式、管線模式，用于描述管道–過濾器這一軟件架構風格的靜態性質；而操作抽象包括管道操作模式、過濾器操作模式、管線操作模式，詳細地描述了管道–過濾器的動態行為。文獻[49]以Z語言的形式化描述為基礎，使用數據抽象和過程抽象，利用關系、函數、集合、序列、包等將數據從數據結構的表示細節中抽象出來，通過組件、連接件的添加及刪除來實現準確描述軟件架構的建模過程。

2. Petri網

Petri網是一種系統的數學和圖形的建模和分析工具，適用于對具有并發、同步、沖突等特點的系統進行模擬和分析，并被廣泛應用于復雜系統的設計與分析中[50]。 Petri網是用于表述分布式系統的眾多數學方法之一，作為一種建模語言，它采用圖形化方法將一個分布式系統結構表述為帶標簽的有向雙邊圖。

Petri網的元素包括庫所（place）、變遷（transition）、有向弧（arc）和令牌（token），其中有向弧存在于庫所和變遷之間，令牌是庫所中的動態對象，可以從一個庫所移動到另一個庫所。Petri網的規則是：有向弧是有方向的，兩個庫所或變遷之間不允許有弧，庫所可以擁有任意數量的令牌[51]。

在軟件架構領域，為了應對軟件動態演化面臨的挑戰，應提高所建立的軟件架構的動態演化性。利用Petri網及其擴展，對面向動態演化的軟件架構進行建模能夠有效提高所建立軟件架構模型的動態演化性。因此，關于利用Petri網對軟件架構建模的研究主要集中在描述軟件架構的動態演化性方面。

經典的軟件架構的Petri網描述是一個四元組，其形式化定義為L=（Cm，Ce，Rr，Ca），其中Cm為軟件架構中的組件，Ce為軟件架構中的連接件，Rr為軟件架構中的角色，Ca為軟件架構中的約束。Petri網形象地描述了軟件架構的動態語義，通過變遷的發射Token從一個庫所分配到另外一個庫所，表明了資源或消息的傳遞，較好地說明了整個軟件系統的流程。Petri網還可以用形式化的分析方法對軟件系統的死鎖和活性進行動態分析和驗證，以進行早期的預防和檢測，避免建模時的人為錯誤，同時可以利用相應的Petri網支持工具對軟件架構模型進行模擬。

文獻[52]提出了一種基于Petri網的軟件架構—PSA（Petri-Software-Architecture）。PSA著眼于有關系統架構全局特性方面的問題，利用Petri網對系統元素間輸入/輸出以及系統靜態、動態特性的描述能力，使用Petri網的可達標識圖給出了一種計算組件貢獻大小的方法，同時還給出了架構演化中組件刪除、增加、修改以及合并與分解等各種變化引起的波及效應分析。通過系統 PSA的可達標識圖（RMG）可以很容易界定某一組件變化所影響的其他組件，即組件對 SA 影響的大小（稱為貢獻或者貢獻大小），比傳統方法[53]中通過系統可達矩陣計算更加直觀，而且組件變化后不一定需要每次重新計算，而可達矩陣方法需要在每次更新系統后重新計算其可達矩陣。

運用基于 PSA模型的可達標識圖來分析軟件架構性能，一方面能給系統架構師提供系統信息參考，如組件貢獻大小可以幫助合適地改變系統架構，同時也可適當地更改原有系統可達標識圖并快速分析變更后新系統的特性；另一方面，首次用 Petri 技術分析系統架構性能為軟件架構研究提供了一個全新的思路。進一步的工作是利用 Petri 網輔助完成軟件架構其他方面的設計，如輔助完成系統運行時的故障診斷與自校正設計。

文獻[54]設計了一種面向動態演化的軟件架構元模型，其選取Petri網作為軟件架構建模的主形式化工具，使得模型在具有直觀圖形表示的同時，又具有精確且嚴格的語義。該軟件架構元模型包括靜態和動態兩個視圖。靜態視圖表達軟件架構的靜態結構，動態視圖以靜態視圖為基礎，反映系統行為導致的軟件架構狀態變化。其中，靜態視圖以Petri網的網結構表示，動態視圖以網系統表示，組件之間的交互就相應地以Petri之間的交互和融合展示出來，軟件系統的動態行為以Petri網中變遷點火引起的網系統的動態運行來展示。通過變遷的分類來映射穩定和易變需求，通過庫所的分類來映射主動和被動需求，通過區分端口和接口來映射計算和交互的相對隔離等機制，在軟件架構建模中繼承和保持需求建模對動態演化的支持機制。

3. B語言

B方法用一種簡單的偽程序語言來描述需求模型、規格說明，并進行中間設計和實現，這個語言就是B語言[55]。B語言支持規格說明的類型檢測、動態驗證、數學證明等以確保設計過程的正確性，同時分層次開發以降低大型軟件開發的復雜性。分層次的方法可以將高層實現表示成低層的規范，一個完整的開發就是逐步實施的規范/實現過程。規范/實現過程在最低級的實現可以從預先實現的可重用的組件庫中得到，高級的重用也可通過不斷擴展新的組件庫從而支持整個開發過程，每一層的實現過程是將規范翻譯成可維護的獨立編譯的源代碼和可執行指令的過程。同其他面向對象方法一樣，B語言中的結構化機制增強了信息隱藏和數據封裝特性，確保了大型開發中各個組件的獨立開發。

B語言使用簡單熟悉的符號表示法[56]。這種符號表示法用廣義替換表示狀態轉換，從規格說明到編碼，這種統一的形式減少了學習的難度和轉換中的語法錯誤，這種“數學程序設計語言”可使人們使用一種非常具體的規格說明形式，而且對軟件工程師來說也是極為有益的。B語言采用模塊化構造，從規格說明到實現的模塊化構造允許將規格說明和驗證過程分解為多個子任務進行，相比其他類似的規格說明語言這個優點是非常突出的，而且比ADA和C++中的結構化構造更容易學習。B語言有大量實用的工具支持，它們支持了B方法中軟件開發周期的所有階段，甚至包括動畫制作和文檔生成等，其他形式化方法似乎還沒有如此強大的類似集成工具。

作為一種較新的、基于模型范疇的形式化方法，B語言將程序和程序規格說明嚴格處于統一的數學框架下，采用基于Zermelo-Frankel集合論的符號表示法書寫。B語言包含一種結構化機制（從需求規格說明到精化再到實現），以一種偽碼語言即抽象機符號表示法（Abstract Machine Notation，AMN）構造需求模型并設計和實現，由于AMN支持規范說明的類型檢測、動態驗證，所以確保了設計過程的正確性。B語言在軟件架構建模領域應用較多，文獻[57]通過分析UML和B語言的優缺點，將二者結合，對UML模型圖使用B語言進行形式化，定義映射規則，并使用B工具Atelier-B對所建模型進行自動檢查與驗證。文獻[58]通過將UML轉換為B AMN，利用Linux下的B語言工具集如BToolKit進行細化、實現及驗證。

4. VDM

VDM是在1969年開發PL/1語言時由IBM公司維也納實驗室的研究小組提出的。VDM是一種功能構造性規格說明技術，它通過一階謂詞邏輯和已建立的抽象數據類型來描述每個運算或函數的功能。20世紀90年代初這種方法在歐美許多研究機構或大學得到了廣泛的應用[59]。

VDM技術的基本思想是運用抽象數據類型、數學概念和符號來規定運算或函數的功能，而且這種規定的過程是結構化的，其目的是在系統實現之前簡短而明確地指出軟件系統要完成的功能。由于這種形式化規格說明中采用了數學符號和抽象數據類型，所以可使軟件系統的功能描述在抽象級上進行，完全擺脫了實現細節，這樣為軟件實現者提供了很大的靈活性。此外，這種形式化規格說明還為程序正確性證明提供了依據。應用VDM技術進行系統開發包含了形式化規格說明、程序實現和程序正確性證明三個部分。

使用VDM定義形式化規格說明具有以下三個明顯的優點：①只告訴計算機做什么；

②提供了程序正確性證明的依據；③使規格說明描述簡練、精確。此外，使用VDM還可以使程序設計者牢固樹立先抽象后具體的不斷證明其正確性的逐步分解、自頂向下的開發思想，從而在整個程序開發的過程中用系統而嚴密的方法來保證所開發程序的正確性。文獻[60]在VDM的基礎上，使用其工具語言Meta-Ⅳ，通過抽象軟件系統的語法域、語義域及語義函數來形式化表示軟件架構的建模過程。文獻[60]利用VDM的擴展語言—面向對象的VDM++，在RUP的分析和設計工作中將UML視圖轉換為相應的VDM++形式化規格說明，以規范軟件架構的建模過程。同時通過VDM++形式化規格說明的每次靜態檢測與模擬執行，確定本次開發周期中所建模的規格說明滿足評價標準的程度，以及在下一次開發周期中可做的改進，通過如此不斷迭代的過程使得軟件規范逐漸滿足評價標準。

5. CSP

CSP即基于進程代數的描述語言，它以進程和進程之間關系的描述為基礎，用來描述一個復雜并發系統的動態交互行為特性。CSP進程通過事件的有序序列來定義。在事件中，一個進程與它的環境相交互。一個進程的所有事件集合構成該進程的字母表。例如αP表示進程P的事件集合，即字母表。事件一般用小寫字母表示，進程用大寫字母表示。對字母表中的不同事件，進程將做出不同的動作，例如x:A→P(x)表示進程P的字母表A中的事件x發生后，進程P以x事件為初始事件繼續進行。進程到某一時刻為止所處理的事件序列定義為進程的跡（trace）。針對復雜進程的描述，CSP允許進程的嵌套，一個大的進程可以由許多小的進程組成。CSP進程之間發送消息交互，進程之間的關系（即進程的組合方式）通過一些運算定義，如順序、并發、選擇、分支以及其他非確定性的交織等。另外，CSP定義了兩個原語進程—Skip（正常終止）和Stop（死鎖），用來終止一個進程。

CSP使用的符號子集包括以下元素[61]：進程和事件，進程描述了交互事件中的一個實體，事件可以是原子的，也可以包含數據，最簡單的進程Stop表示沒有事件；前綴，如果有e→P，則e為P的前綴；替代（alternative），即確定性選擇，一個進程可以表現為P或Q，由它自己決定，表示為PΠQ；決定（decision），非確定性選擇，一個進程可以表現為P或Q，且由它所處的環境（與其他過程的交互）決定，表示為P[]Q；命名進程（named process），進程名稱可以與進程的表達式相關聯。

CSP以事件為核心，通過事件集合實現進程及其關系的描述，并且通過失效/偏差模型對進程行為進行判別。失效由跡和拒絕集成對定義，拒絕集也是一個事件集合，它給出進程在指定跡上面可以拒絕的事件集合。偏差用于描述無法預測的環境。CSP的主要優點在于CSP規范的可執行特性，因此可以檢查內在的一致性。此外，CSP還支持從規范驗證到設計和實現的一致性，即如果規范是正確的，并且轉換也是正確的，那么設計和實現也是正確的。CSP不僅可以用于建立刻畫系統行為的模型，還可以用于建立推理的形式演算模型，研究者們發現CSP能夠很好地描述軟件架構模型的各種語義屬性。文獻[62]在CSP理論的基礎上，對軟件架構的形式語義和代數語義進行了分析，并對軟件架構的元模型進行了描述，將元模型的每一層都描述為一個進程，然后利用CSP嚴密的語義特性表達能力和演算推理分析能力對整個模型進行良好的語義描述分析和檢測。

軟件開發 架構設計 軟件

版權聲明：本文內容由網絡用戶投稿，版權歸原作者所有，本站不擁有其著作權，亦不承擔相應法律責任。如果您發現本站中有涉嫌抄襲或描述失實的內容，請聯系我們jiasou666@gmail.com 處理，核實后本網站將在24小時內刪除侵權內容。

版權聲明：本文內容由網絡用戶投稿，版權歸原作者所有，本站不擁有其著作權，亦不承擔相應法律責任。如果您發現本站中有涉嫌抄襲或描述失實的內容，請聯系我們jiasou666@gmail.com 處理，核實后本網站將在24小時內刪除侵權內容。