上海同濟大學 馬 亮
CHAM軟件連接形式化模型研究
上海同濟大學 馬 亮
CHAM形式化模型以代數演算的方式研究通信并發系統,將進程看作是代標號的變遷系統,遷移的規則是以句法重新安排的方式來反映狀態信息的變化過程。
1.CHAM形式化模型結構。CHAM形式化模型最初是由Berry和Boudol開發研制的,它建立在化學隱喻的基礎上。CHAM形式化模型中的各個結構都可以利用化學概念來描述,CHAM形式化模型主要包括分子(Molecules)、溶液(Solutions)以及膜(Membrane)結構。
(1)分子。分子是組成CHAM形式化模型的進本元素,由進程代數理論可知,子結構主要是由一些基本常量和操作細節所組成,分別用m1,m2,…,mn來表示。
(2)溶液。溶液是多分子的集合體,可以表示為S = m1,m2,…,mn,而且有多個溶液組成的一個較大型的溶液還可以表示為S∪S′ = m1,m2,…,mn,m1′,m2′,…,mn′,在CHAM形式化模型中溶液可以定義為一個狀態信息。
(3)膜結構。膜結構是對CHAM形式化模型的各種結構進行封包分層細化,可以表示為{︱.︱},利用膜結構可以將不同溶液進行封包,此時就可以將被封裝的溶液看作是一個單一分子,即為{︱S = m1,m2,…,mn︱}。而且膜結構還具有一定的選擇透過性,即通過膜上的氣孔,對分子的進入和離開進行選擇,這一過程可以表示為S′= mi{︱m1,m2,…,mn︱}。
2.CHAM形式化模型遷移規律。分為一般反應和特定反應兩大類。一般反應是對所有的CHAM形式化模型描述的軟件體系結構都有效,沒有任何限制;特定反應只是針對某一具體的CHAM形式化模型進行描述,是一種無任何前置條件的基本項重寫規則。
1.CHAM形式化模型的構建元素。包括處理元素、數據元素、連接元素、膜元素四種基本構件元素。
(1)處理元素。處理元素可以表示為分子結構,具體是指具有一定功能的邏輯處理對象或者單元,在進行軟件體系結構描述的過程中也可以代表軟件的構件單元。CHAM形式化模型的處理元素主要是由接口描述以及狀態定義兩大部分構成。其中接口描述包括一組說明處理元素與外部環境交互的端口,而狀態定義則是用來描述軟件的構件單元的當前狀態。
(2)數據元素。數據元素主要包括進行軟件結構描述所使用和變化的信息,通常,數據元素用依附在處理元素的紅色和藍色三角形來表示;紅色三角形代表從處理元素中輸入的數據元素,而藍色三角形則代表從處理元素輸出的數據元素。
(3)連接元素。連接元素的主要作用是將體系結構中的各個成分連接在一起。例如,在不同處理元素之間進出的有效通訊元素就屬于連接元素。而且每一個連接元素都具有連接不同處理元素之間的交互條件,也就是CHAM形式化模型中的反應規則,一般情況下用圓圈表示連接元素。
(4)膜元素。膜元素是由一些處理元素和連接元素根據行對應的要求組合而成的,可以通過膜上的氣孔實現處理元素的輸出與輸入。
2.CHAM形式化模型的實現。CHAM形式化模型的實現主要應用Java語言,在NIST/ECMA環境集成的參考模型來構建。建模過程包括指圖形視圖和文本視圖兩大部分,圖形視圖和文本視圖建立在同一數據模型的基礎上。先以Shape基類為根節點,然后派生出Process類、Date類、Membrane類、Port類數據模型。通過面向對象語言的多態性等特征,就可以將一些例如繪制、移動以積分放縮等相同的操作或者函數歸于同一基類中。再根據DRTSADL的語法建立數據模型元素間的樹形結構,通過這種樹形結構在方便實現數據模型元素導航的同時也更有利于Java序列化存儲。使用CHAM形式化模型的基本建模元素設計軟件體系結構圖,并且在構圖的同時還可以進行模型語義一致性檢查等工作。在設計軟件體系結構圖功能時,使用了職責鏈設計模式,即在加入其他新建模元素類時,不會對原先的系統造成任何影響。文本視圖建模主要包括程序理解以及信息瀏覽兩大功能,程序理解部分主要是由軟件架構師根據圖形建模生成的或者手工編寫的CHAM形式化模型的描述并最終生成CHAM形式化模型的層次結構。源文件的瀏覽顯示CHAM形式化模型的文件內容,包括關鍵字、操作符等內容。另外,由于圖形視圖和文本視圖建立在同一數據模型的基礎上,因此更有利于兩者間的數據轉換。從軟件體系結構圖生成CHAM形式化模型的文本的過程來分析,兩者之間的數據交換主要是按照CHAM形式化模型的語法結構,直接從數據模型中抽取文本,屬于一個正向的過程。而從CHAM形式化模型的文本產生軟件體系結構圖則屬于一個逆向過程,因為文本視圖所映射的數據模型知識和圖形視圖所映射的數據模型子集不包含圖形視圖的布局信息,需要通過軟件結構配置語義生成對應的布局信息,并且要確保布局的合理性以及有效性。
隨著軟件技術的快速發展,各行各業對于軟件的使用和依賴性越來越高,CHAM軟件是一款專門用來描述各類軟件系統動態行為的一種工具,廣泛應用于各類軟件的體系結構及行為的描述和分析。本文,筆者以CHAM形式化模型為主要研究對象,重點介紹了CHAM形式化模型的特點以及CHAM軟件構建形式化模型的主要工作原理,并且詳細分析了該模型的設計與實現,對建立系統、完善的計算機軟件質量評價體系具有一定的指導意義。