基于Event-B的細化需求建模及驗證

史逸軒，王鴻斌

（忻州師范學(xué)院 計算機系，山西 忻州 034000）

1 引言

絕大多數(shù)系統(tǒng)建模已定型，意味著系統(tǒng)若想要補充新的功能是非常困難甚至于不可能實現(xiàn)。Event-B的細化功能為擴展系統(tǒng)功能提供了新思路。Event-B格式內(nèi)，所有events均可細化，在events里添加限制條件，如：時間、地點、數(shù)量等，通過改變環(huán)境、常量和變量的設(shè)置來具體化、細節(jié)化events，從而實現(xiàn)更多的系統(tǒng)功能。

細化的中心思想是分解，將events分解為子模型令其各自獨立細化。細化的最普遍的模式是：將理想化結(jié)果作為抽象的原模型，之后將其分解為子模型進行細化，適用于時序式系統(tǒng)、并發(fā)式系統(tǒng)和分布式系統(tǒng)[1]。

依據(jù)Jean Raymond理論，細化可分為兩大類。一類稱為水平細化，是抽象豐富的過程。某些情況下，系統(tǒng)太過復(fù)雜而難以一次性完成，水平細化會將系統(tǒng)抽象為若干個部分，然后對每部分添加更多問題或要求，豐富每個部分進而豐富系統(tǒng)功能。另一類稱為垂直細化，通常發(fā)生在水平細化過程完成之后，此時系統(tǒng)功能已經(jīng)擴展，只需要對數(shù)據(jù)和變換關(guān)系進行轉(zhuǎn)換使其更容易在計算機上實現(xiàn)。

2 Event-B細化需求建模示例

Event-B細化建模同樣是在Rodin中編寫events并驗證其有效性。Rodin平臺是用于支持系統(tǒng)開發(fā)的開放工具集，包含模型數(shù)據(jù)庫及多種插件，如：靜態(tài)檢查器、驗證規(guī)約生成器、模型檢查器、UM L轉(zhuǎn)換器和需求文檔處理器等，而數(shù)據(jù)庫本身包含基本變量、常量和轉(zhuǎn)換關(guān)系[2]，多種構(gòu)建離散轉(zhuǎn)換系統(tǒng)模型所需的模型元素。

以賬單分攤系統(tǒng)為例，完成系統(tǒng)需求分析、Event-B建模和驗證之后，添加時間日期作為限制條件。由此可見，要實現(xiàn)時間日期細化，分布式應(yīng)用必須基于能夠處理時間約束的算法且要強制將時間約束表達為數(shù)學(xué)模型，所采用的方法是在Event-B的細化建模階段集成時間約束[3]。該系統(tǒng)的數(shù)據(jù)細分也是基于上述理論。綜上所述，賬單分攤系統(tǒng)有以下三點需求可被細化：

（1）添加成員支付其賬單份額的日期和時間；

（2）添加賬單全部付清的日期和時間；

（3）添加成員加入小組的起始日期和退出小組的結(jié)束日期，當(dāng)且僅當(dāng)成員還是小組成員時，列出在其加入的每個小組內(nèi)的應(yīng)付賬單份額。

2.1 高級規(guī)范化細化需求建模

細化需求建模時同樣需要為所有細化需求設(shè)置以下的環(huán)境、變量和常量。

（1）環(huán)境：細化需求建模時，不需要設(shè)置新集合，依然是用戶和小組兩個集合（見圖1）。

圖1：細化-環(huán)境Figure1:Refinement-Context

（2）變量：變量設(shè)置不變，將每一個變量與日、月、年、時和分相關(guān)聯(lián)即可，所有變量初始化均為空集（如圖 2）。

圖2：細化-變量Figure 2:Refinement-Variables

（3）常量：下述所列的所有常量，僅允許被細化模型訪問：時、分、日、月和年是五個在被與其相關(guān)的功能所調(diào)用之前需要填入元素的集合。這五個集合只允許填入符合邏輯的值（例如：一小時的值要介于00-23，一分鐘的值介于00-59，一天的值介于00-31）。將其余常量bill_paid，share_paid，joining_group 和leave_group這幾個功能以日、月和年劃分開，將這些信息作為數(shù)字來處理，從而避免去新建一個D A T E類，并且可以對這些數(shù)值進行比較。當(dāng)與b ill_pa i d功能相關(guān)聯(lián)時，需要進一步以時間的時、分來細化（如圖3）。

圖3：細化-常量Figure 3:Refinement-Invariants

2.2 細化Events

使用上述環(huán)境、變量和常量來表達對應(yīng)關(guān)系并對每個細化需求（event）建模。

細化需求（1）：添加成員支付其賬單份額的日期和時間

成員支付賬單份額發(fā)生在以下三個events中：Members_pay_bill，Member_pays_initially和 Members_repay_bill。從上述第一條細化需求可得出，每當(dāng)有成員支付其賬單份額時，就需要添加發(fā)生的時間和日期。條件 6（@gr d6）、7（@gr d7）、10（@gr d10）、11（@grd11）和12（@grd12）用于確保時間和日期以正確的格式添加。條件 8（@gr d8）和 9（@gr d9）檢查確保要添加的小時和分鐘還未存在于當(dāng)前集合share_paid_hour和share_paid_minute中。條件13（@gr d13）、14（@gr d14）和 15（@gr d15）檢查添加日期是否已經(jīng)存在于集合share_paid_day，share_paid_month和share_paid_year中。Events中發(fā)生的的所有行為（@act）就是將日期，時間和該成員支付的份額數(shù)值一起添加入正確合適的集合中。Members_pay_bill，Member_pays_initially 和 Members_repay_bill三個集合中的條件行為都相同，唯一的區(qū)別在于Members_repay_bill中行為的編號不同，故均以圖4為代表。

細化需求（2）：添加賬單全部付清的日期和時間

圖4：細化-成員支付份額Figure 4:Refinement-Members pay his share

當(dāng)賬單全部付清后，會從待付賬單集合中移出。據(jù)第二條細化需求的要求，賬單付清時需要添加日期和時間。條件 5 （@gr d5）、6（@gr d6）、9（@gr d9）、10（@gr d10）和 11（@gr d11）確保添加的時間和日期的格式正確。條件7（@gr d7）和8（@gr d8）檢查確保要添加的小時和分鐘還不存在于集合bill_paid_hour和bill_paid_minute中。條件12（@gr d12）、13（@gr d13）和 14（@gr d14）檢查要添加的日期是否已存在與集合bill_paid_day，bill_paid_month，和 bill_paid_year中。Event的行為（@act）均為將日期，時間和相應(yīng)的已付清賬單的數(shù)值一起添加進恰當(dāng)?shù)募现校ㄈ鐖D5）。

圖5：細化-移出付清賬單Figure 5:Refinement-Remove fully settled bill

細化需求（3）：添加成員加入小組的起始日期和退出小組的結(jié)束日期，當(dāng)且僅當(dāng)成員還是小組成員時，列出在其加入的每個小組內(nèi)的應(yīng)付賬單份額。

為達到成員能夠看到自己所加入的每個小組中應(yīng)支付的賬單份額的目的，需要在適當(dāng)?shù)募现刑砑釉摮蓡T加入每一個小組的日期，以及該成員退出每個小組的日期。Add Member Group中條件4（@gr d4）、5（@gr d5）和 6（@gr d6）檢查確保試圖添加的日期格式正確。條件 7（@gr d7）、8（@gr d8）和 9（@gr d9）檢查需要添加的日期是否已經(jīng)存在于集合join_group_day，join_group_month 和 join_group_year中。所有行為（@act）均是將日期與對應(yīng)的該成員加入的小組添加到適當(dāng)?shù)募现校ㄒ妶D6）。

Remove Member Group中的所有行為（@act）和條件（@grd）都類似于Add Member Group，區(qū)別僅在于與它相關(guān)聯(lián)的日期不是join_group的日期，而是leave_group的日期。當(dāng)某成員退出小組時，意味著該成員不再是小組的成員，那么需將其的join_group日期刪除（見圖6）。

圖6：細化-成員加入/退出小組Figure 6:Refinement-Add/Remove amemberto/from a group

Deregister Member中所有條件（@grd）都與Remove Member Group完全相同。二者之間的區(qū)別僅在于活動（@act），當(dāng)成員徹底從系統(tǒng)中注銷時，需將join_group和l eave_group的日、月和年全部刪除（見圖7）。

圖7：細化-成員注銷Figure 7:Refinement-Deregister member

為每位成員和小組添加join_group和leave_group之后，需要列出某位成員所加入的每個小組中應(yīng)付賬單份額的數(shù)值，條件7（@grd7）、8（@grd8）和9（@gr d9）確保當(dāng)前日期是正確的格式。條件10（@gr d10）確保該成員已經(jīng)加入該小組，或者檢查該成員是否今天退出了小組，也就是說某成員退出小組時，便不能夠再去查看他在這組的賬單份額的信息。條件11（@gr d11）確保當(dāng)前日期在該成員加入該小組的日期之后，也就是說某成員只有在加入小組之后，才能夠查看他在小組中的賬單份額信息（如圖 8）。

圖8：細化-列出成員在每個小組的賬單份額Figure 8:Refinement-Listallshares of a member at each of his group[4]

3 Pro-B規(guī)范化驗證

與普通events相同，細化需求后的events也使用P ro-Banimator進行規(guī)范化驗證。以下是規(guī)范驗證的步驟流程。

第一步：初始化之前（如圖9）

圖9：細化初始化前Figure 9:Before Refinement In itializatio

第二步：執(zhí)行初始化event

所有模型中的變量在S tate窗口中為初始化默認值（如圖 10）。

第三步：執(zhí)行細化events

初始化之后，可運行的events 如下：Add_share，Add_initial_bill，RegisterMember，AddDate和CreateGroup。添加成員，創(chuàng)建小組并加入日期和時間（日，月，年，時，分）之后，AddMemberGroup，DeregisterMember，Add_initial_bill和add_share功能隨即被激活。在抽象機制中， 若執(zhí)行AddMemberGroup 功能，RemoveMemberGroup 和ListMemberGroup 隨即被激活[5]。細化機器中，需要將join_date加入恰當(dāng)?shù)募现?，RemoveMemberGroup 中也要加入leave_date,同時DeregisterMember 中要將join_date 和leave_date都刪除。

當(dāng)賬單已添加入Add_initial_bill 且Group 已加入到CreateGroup 時，Add_group_Bill 激活并將賬單分配到小組中，隨后Add_member_share 觸發(fā)并將賬單份額分配給組中成員。Add_member_share執(zhí)行后，像在抽象機制中一樣，支付賬單的兩種方式隨即被激活。若小組中某成員支付賬單全額，bill_date的時間的日期將被添加入相應(yīng)的集合中。

圖10：細化初始化Figure 10:Refinement-Initialization

賬單全額付清時，該賬單從小組中刪除之前會重寫bill_paid時間和日期集合，并且將該賬單添加入paid_db集合中[6]。

全部執(zhí)行的events的所有最終值如圖11所示。

圖11：執(zhí)行細化Figure 11:Refinement-Execution

4 結(jié)論

通過賬單分攤系統(tǒng)細化需求建模和驗證的例子，可以看出E vent-B細化需求建模方法是當(dāng)前擴展系統(tǒng)功能最為簡便高效的方法，彌補了傳統(tǒng)系統(tǒng)建模方法的缺陷。眾所周知，軟件危機是當(dāng)前軟件工程所面臨的巨大危機，而解決這一危機的公認的有效方法是實現(xiàn)軟件復(fù)用。軟件復(fù)用的途徑有很多，例如基于構(gòu)件的開發(fā)方法。若能降低擴展系統(tǒng)功能的難度以及消耗，無疑會增強軟件復(fù)用度。