基于CCS的軟件規(guī)范描述及實例

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

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

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

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

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

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

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

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

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

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

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

12、用一個類VendingMachine模擬模擬, 轉(zhuǎn)換規(guī)則如下，整個轉(zhuǎn)換用轉(zhuǎn)換規(guī)則如下，整個轉(zhuǎn)換用手工實現(xiàn)：手工實現(xiàn)： class VendingMachine int state;/數(shù)組元素對應(yīng)的各端口的狀態(tài)，置數(shù)組元素對應(yīng)的各端口的狀態(tài)，置0表示關(guān)閉端口，置表示關(guān)閉端口，置1表示開表示開放端口：放端口： /state0-1p,state1-2p,state2-little,state3-big,state4-collect int money;/錢的數(shù)量錢的數(shù)量 int number;/收集盤中巧克力的個數(shù)收集盤中巧克力的個數(shù) VendingMachine();/構(gòu)造方法構(gòu)造方法 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、/創(chuàng)建創(chuàng)建GUI組件，添加用戶界面事件映射關(guān)系組件，添加用戶界面事件映射關(guān)系 main();/主函數(shù)主函數(shù) 系統(tǒng)實現(xiàn)系統(tǒng)實現(xiàn) 系統(tǒng)進程表達式的無限循環(huán)等待 系統(tǒng)實現(xiàn)系統(tǒng)實現(xiàn) 系統(tǒng)動作對應(yīng)類VendingMachine中的方法系統(tǒng)實現(xiàn)系統(tǒng)實現(xiàn) 系統(tǒng)進程表達式中不同動作之間用“+”表示的非確定性選擇對應(yīng)著機器端口與客戶的相互作用非確定性選擇對應(yīng)著機器端口與客戶的相互作用，采用用戶界面事件觸發(fā)機制實現(xiàn)。 系統(tǒng)實現(xiàn)系統(tǒng)實現(xiàn) 以進程表達式的定義反映的系統(tǒng)約束條件對應(yīng)著VendingMachine對象中的方法調(diào)用序列 系統(tǒng)實現(xiàn)系統(tǒng)實現(xiàn)系統(tǒng)進程表達式與動作方法的實現(xiàn)過程沒有直接的映射關(guān)系，我們可以通過系統(tǒng)進

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