1、基于CCS的軟件規范描述及Java實例高春鳴高春鳴軟件規范描述方法 軟件規范描述方法主要是軟件工程化的UML方法與形式化方法二類方法。形式化方法采用數學方法來描述、建模、分析和自動化軟件。目前形式化方法主要流行的是Z、B、VDM和包括RAISE6在內的一批以謂詞邏輯和集合論為基礎的形式化規格說明語言。這些規格說明語言給出系統（程序）狀態和狀態變換操作的顯式抽象定義，覆蓋了從規范說明到編碼過程的開發方法5。他們所用的符號和方法支持大部分的軟件過程：需求分析、規格說明、軟件設計、實現和維護。目前形式化方法主要存在的問題有：（1）類似Z、B的形式化規格說明語言，其實際規范和實際代碼間的差異很大。（2

2、）由于Z、B形式化方法本身的特點，形式化方法和軟件開發過程較難平滑地結合起來。基于進程代數的形式化描述方法 相對于邏輯方法,基于進程代數的模型和形式化描述方法能夠刻畫更為細致的系統行為關系。 CCS是進程代數方法的代表,它具有很好的代數性質,不僅有刻畫系統行為的模型還具有進行推理的形式演算系統1，所以說CCS方法既有模型又有演算。此外,CCS還用互模擬關系刻畫進程間的等價關系,實際上保證了系統規范和實現的語義一致性.本文首先用CCS演算描述系統需求規格，隨后提出了帶約束條件的CCS的概念。利用這個新的定義抽取了系統規范，最后用Java語言實現了系統原型代碼。 CCS的定義的定義 語法語法 進程

3、可用下面BNF刻畫其語法: E:=Nil|A|.E|E+E|E|E|EL|Ef 在進程E的表示中：Nil是終止的進程或死鎖的進程,不再執行任何動作,常用0表示；A表示常量；.E是前綴操作項,描述動作先后執行序列；+是求和操作項,多個項求和時，記做,描述進程的不確定選擇,至少有一個進程執行；|是組合操作項,描述兩個進程的并行執行;是限定操作項,描述具有標記的動作,在進程中不能執行;是換名映射操作項。 操作語義操作語義 派生樹和進程遷移圖派生樹和進程遷移圖 為了演示如何使用上述操作規則,我們利用派生樹推導。來展示一個實時系統的各種行為.假設有一進程表達式為: 圖1表示了它對應的派生樹。 在進程遷移

4、圖中,進程以及進程間的交互行為,既可以用圖表示方法，其中一個圖可以對應一個進程,圖之間的歸約對應進程之間的交互行為。一般是通過合并一個派生樹中代表相同的表達式的節點而得到的進程遷移圖。 0 .) 0 .0 .( . rrP設派生樹和進程遷移圖派生樹和進程遷移圖 我們采用CCS建模方法是基于進程遷移圖向進程表達式轉換的思路。我們根據系統需求，畫出進程派生樹，通過合并一個派生樹中代表相同的表達式的節點而得到進程遷移圖，然后根據結構操作語義和系統約束條件得到進程表達式。并且實現了進程表達式和圖之間的手工轉換形式。 實例研究實例研究 我們用CCS演算描述系統需求規格，并抽取了系統規范，用Java語言實

5、現了系統原型代碼。系統的原型是一個自動售貨機1，如下是一個銷售巧克力的自動售貨機的圖。我們設定大的巧克力要花費2角錢，小的巧克力要花費1角錢，為簡化起見，自動售貨機的投幣孔只能投2角或1角錢硬幣（假設有2角錢硬幣）。該自動售貨機工作流程是：買巧克力，從投幣孔投一個1角或2角錢的硬幣開始，客戶可以繼續投幣，但是不能超過4角錢，也可以按大巧克力或小巧克力按扭，接著若收集盤中有巧克力則從取貨盤處取走巧克力。自動售貨機的動作按下列嚴格的規定：售貨機既不會占客戶的便宜又不會自己吃虧；在投幣達到4角錢后，兩個投幣孔不能再投入任何硬幣；取貨盤只能裝一只巧克力，在取貨盤處已有一只巧克力時，售貨機鎖住兩個按扭和

6、投幣孔，客戶不能再次投幣；在按了按扭之后，必須從取貨盤處取走巧克力，才能再次投幣。 系統約束條件 歸納以上自然語言描述的系統需求，系統約束條件為：貨物價格：大的巧克力要花費2角錢，小的巧克力要花費1角錢；投幣孔限制：2角投幣孔投2角錢硬幣，1角投幣孔投1角錢硬幣；售貨機工作流程限制：買巧克力，從投幣孔投一個1角或2角錢的硬幣，然后按大巧克力或小巧克力按扭，接著必須從取貨盤處取走巧克力。取貨盤只能裝一只巧克力，在取貨盤處已有一只巧克力時，售貨機鎖住按扭和兩個投幣孔，客戶不能再次投幣；在按了選擇巧克力按扭之后，必須從取貨盤處取走巧克力，才能再次投幣。沒有按選擇巧克力按扭之前，巧克力不能落入取貨盤處

7、。售貨機原則：不容許投幣之后，出現不能售出相應價值的巧克力；也不能售出多于投幣價值的巧克力；不容許投幣之后，出現機器不能處理的情況，而需要退還客戶的硬幣。售貨機內金額限制：在投幣達到4角錢后，兩個投幣孔不能再投入任何硬幣。 采用采用CCS演算描述系統需求演算描述系統需求 采用采用CCS演算描述系統需求演算描述系統需求 1角孔 2角孔 大按扭 小按扭 取貨盤1p2pbiglittlecollect系統規范 根據系統約束條件和操作語義，參照系統進程遷移圖，系統進程表達式的定義如下，也即系統規范的一個具體實現： 系統進程遷移圖 系統的行為分析 整個系統的行為分析，從進程遷移圖可以看到，系統存在無限的

8、狀態循環路徑，如連續2次投入2角硬幣，可到達系統w(4p,0)狀態，接著做big, 動作，客戶可取出一支小的巧克力，到達w(2p,0)狀態，客戶這時既可繼續做選擇和取巧克力的工作，消耗已投硬幣金額，也可又投入2角硬幣，重新達到w(4p,0)狀態，所以系統狀態遷移存在無限的狀態循環路徑。以下是該無限的狀態循環路徑的進程表達式表示： collect無限的狀態循環路徑的進程表達式系統規范 系統規范 系統規范抽象了系統的行為，但由于在規范中還存在著系統模型常量，故當模型改系統規范抽象了系統的行為，但由于在規范中還存在著系統模型常量，故當模型改變時，這些常量也變化，上述方程式描述的系統規范將作廢。這是因

9、為采用純變時，這些常量也變化，上述方程式描述的系統規范將作廢。這是因為采用純CCS描述的系統規范的抽象程度有限，系統的約束條件無法加入到規范之中，所以此規描述的系統規范的抽象程度有限，系統的約束條件無法加入到規范之中，所以此規范不能作為軟件形式化規格描述。因此，我們提出了帶約束條件的范不能作為軟件形式化規格描述。因此，我們提出了帶約束條件的CCS的概念，這的概念，這樣就可以把系統的約束條件顯式的表現在進程表達式中。比如表達式中樣就可以把系統的約束條件顯式的表現在進程表達式中。比如表達式中“(money+xi )=4p xi”代表遍歷代表遍歷Xi的定義域中滿足的定義域中滿足“(money+xi

10、)=4p”這個約這個約束條件的值的集合，這個是非確定選擇。我們對自動售貨機的規范重新描述如下：束條件的值的集合，這個是非確定選擇。我們對自動售貨機的規范重新描述如下： 軟件行為等價判定 i）規范與規范：對描述多進程且狀態復雜的大型系統屏蔽系統的內部動作，采取抽取系統外部行為描述作為系統規約，并在系統規約與系統的軟件實現間形成互模擬關系。這樣可在系統軟件規約與系統軟件實現多個層次的不同粒度的軟件行為互模擬驗證； ii）規范與實現：抽象規范與具體實現之間的互模擬驗證； iii）實現與實現：對同一個規范的不同實現的互模擬驗證。 系統實現系統實現 我們對系統進行了軟件模擬，將系統進程表達式向我們對系統

11、進行了軟件模擬，將系統進程表達式向Java程序轉換，程序轉換，CCS的語的語法符號對應著程序構件法符號對應著程序構件, 一個進程的進程遷移圖對應一個進程，一個進程對一個進程的進程遷移圖對應一個進程，一個進程對應一個類，一個進程對應一組進程表達式；一個動作對應一個方法，方法的應一個類，一個進程對應一組進程表達式；一個動作對應一個方法，方法的參數就是類的狀態變量；動作前置、后置條件（約束條件，設置下一步的動參數就是類的狀態變量；動作前置、后置條件（約束條件，設置下一步的動作端口、通道開閉）通過手工向類中的方法做映射。作端口、通道開閉）通過手工向類中的方法做映射。整個自動售貨機用一個類整個自動售貨機

12、用一個類VendingMachine模擬模擬, 轉換規則如下，整個轉換用轉換規則如下，整個轉換用手工實現：手工實現： class VendingMachine int state;/數組元素對應的各端口的狀態，置數組元素對應的各端口的狀態，置0表示關閉端口，置表示關閉端口，置1表示開表示開放端口：放端口： /state0-1p,state1-2p,state2-little,state3-big,state4-collect int money;/錢的數量錢的數量 int number;/收集盤中巧克力的個數收集盤中巧克力的個數 VendingMachine();/構造方法構造方法 void

13、pressLittle(int money, int number)；/處理處理little按扭方法按扭方法 void pressBig(int money,int number)；/處理處理big按扭方法按扭方法 void put1P(int money,int number)；/處理投處理投1硬幣方法硬幣方法 void put2P(int money,int number),；/處理投處理投2個硬幣方法個硬幣方法 void collectChocolate(int money,int number)；/處理收集巧克力方法處理收集巧克力方法 void createComponents ();

14、/創建創建GUI組件，添加用戶界面事件映射關系組件，添加用戶界面事件映射關系 main();/主函數主函數 系統實現系統實現 系統進程表達式的無限循環等待 系統實現系統實現 系統動作對應類VendingMachine中的方法系統實現系統實現 系統進程表達式中不同動作之間用“+”表示的非確定性選擇對應著機器端口與客戶的相互作用非確定性選擇對應著機器端口與客戶的相互作用，采用用戶界面事件觸發機制實現。 系統實現系統實現 以進程表達式的定義反映的系統約束條件對應著VendingMachine對象中的方法調用序列 系統實現系統實現系統進程表達式與動作方法的實現過程沒有直接的映射關系，我們可以通過系統進

15、程表達式與動作方法的實現過程沒有直接的映射關系，我們可以通過動作方法中的代碼間接實現系統的約束條件動作方法中的代碼間接實現系統的約束條件 public void put1p(int money, int number)/判斷判斷1p端口是否開放端口是否開放if(state0!=1) System.out.println(“非法操作！非法操作！”)； Return; /執行執行1p動作改變系統狀態動作改變系統狀態this.money=money+1; /投入投入1角錢，角錢，money加加1this.number=number; /投幣動作不影響巧克力個數，巧克力個數不變投幣動作不影響巧克力個數，巧克力個數不變 /根據系統狀態以及系統約束條件設置下一步五個端口的狀態根據系統狀態以及系統約束條件設置下一步五個端口的狀態if(this.money+1)=4) this.state0=1; /開放