基于Event-B的細(xì)化需求建模及驗(yàn)證

史逸軒，王鴻斌

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

1 引言

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

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

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

2 Event-B細(xì)化需求建模示例

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

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

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

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

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

2.1 高級(jí)規(guī)范化細(xì)化需求建模

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

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

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

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

圖2：細(xì)化-變量Figure 2:Refinement-Variables

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

圖3：細(xì)化-常量Figure 3:Refinement-Invariants

2.2 細(xì)化Events

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

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

成員支付賬單份額發(fā)生在以下三個(gè)events中：Members_pay_bill，Member_pays_initially和 Members_repay_bill。從上述第一條細(xì)化需求可得出，每當(dāng)有成員支付其賬單份額時(shí)，就需要添加發(fā)生的時(shí)間和日期。條件 6（@gr d6）、7（@gr d7）、10（@gr d10）、11（@grd11）和12（@grd12）用于確保時(shí)間和日期以正確的格式添加。條件 8（@gr d8）和 9（@gr d9）檢查確保要添加的小時(shí)和分鐘還未存在于當(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í)間和該成員支付的份額數(shù)值一起添加入正確合適的集合中。Members_pay_bill，Member_pays_initially 和 Members_repay_bill三個(gè)集合中的條件行為都相同，唯一的區(qū)別在于Members_repay_bill中行為的編號(hào)不同，故均以圖4為代表。

細(xì)化需求（2）：添加賬單全部付清的日期和時(shí)間

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

當(dāng)賬單全部付清后，會(huì)從待付賬單集合中移出。據(jù)第二條細(xì)化需求的要求，賬單付清時(shí)需要添加日期和時(shí)間。條件 5 （@gr d5）、6（@gr d6）、9（@gr d9）、10（@gr d10）和 11（@gr d11）確保添加的時(shí)間和日期的格式正確。條件7（@gr d7）和8（@gr d8）檢查確保要添加的小時(shí)和分鐘還不存在于集合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）均為將日期，時(shí)間和相應(yīng)的已付清賬單的數(shù)值一起添加進(jìn)恰當(dāng)?shù)募现校ㄈ鐖D5）。

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

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

為達(dá)到成員能夠看到自己所加入的每個(gè)小組中應(yīng)支付的賬單份額的目的，需要在適當(dāng)?shù)募现刑砑釉摮蓡T加入每一個(gè)小組的日期，以及該成員退出每個(gè)小組的日期。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）均是將日期與對(duì)應(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)某成員退出小組時(shí)，意味著該成員不再是小組的成員，那么需將其的join_group日期刪除（見圖6）。

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

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

圖7：細(xì)化-成員注銷Figure 7:Refinement-Deregister member

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

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

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

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

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

圖9：細(xì)化初始化前Figure 9:Before Refinement In itializatio

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

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

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

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

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

圖10：細(xì)化初始化Figure 10:Refinement-Initialization

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

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

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

4 結(jié)論

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