基于Event-B的细化需求建模及验证

史逸轩，王鸿斌

（忻州师范学院 计算机系，山西 忻州 034000）

1 引言

绝大多数系统建模已定型，意味着系统若想要补充新的功能是非常困难甚至于不可能实现。Event-B的细化功能为扩展系统功能提供了新思路。Event-B格式内，所有events均可细化，在events里添加限制条件，如：时间、地点、数量等，通过改变环境、常量和变量的设置来具体化、细节化events，从而实现更多的系统功能。

细化的中心思想是分解，将events分解为子模型令其各自独立细化。细化的最普遍的模式是：将理想化结果作为抽象的原模型，之后将其分解为子模型进行细化，适用于时序式系统、并发式系统和分布式系统[1]。

依据Jean Raymond理论，细化可分为两大类。一类称为水平细化，是抽象丰富的过程。某些情况下，系统太过复杂而难以一次性完成，水平细化会将系统抽象为若干个部分，然后对每部分添加更多问题或要求，丰富每个部分进而丰富系统功能。另一类称为垂直细化，通常发生在水平细化过程完成之后，此时系统功能已经扩展，只需要对数据和变换关系进行转换使其更容易在计算机上实现。

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

Event-B细化建模同样是在Rodin中编写events并验证其有效性。Rodin平台是用于支持系统开发的开放工具集，包含模型数据库及多种插件，如：静态检查器、验证规约生成器、模型检查器、UM L转换器和需求文档处理器等，而数据库本身包含基本变量、常量和转换关系[2]，多种构建离散转换系统模型所需的模型元素。

以账单分摊系统为例，完成系统需求分析、Event-B建模和验证之后，添加时间日期作为限制条件。由此可见，要实现时间日期细化，分布式应用必须基于能够处理时间约束的算法且要强制将时间约束表达为数学模型，所采用的方法是在Event-B的细化建模阶段集成时间约束[3]。该系统的数据细分也是基于上述理论。综上所述，账单分摊系统有以下三点需求可被细化：

（1）添加成员支付其账单份额的日期和时间；

（2）添加账单全部付清的日期和时间；

（3）添加成员加入小组的起始日期和退出小组的结束日期，当且仅当成员还是小组成员时，列出在其加入的每个小组内的应付账单份额。

2.1 高级规范化细化需求建模

细化需求建模时同样需要为所有细化需求设置以下的环境、变量和常量。

（1）环境：细化需求建模时，不需要设置新集合，依然是用户和小组两个集合（见图1）。

图1：细化-环境Figure1:Refinement-Context

（2）变量：变量设置不变，将每一个变量与日、月、年、时和分相关联即可，所有变量初始化均为空集（如图 2）。

图2：细化-变量Figure 2:Refinement-Variables

（3）常量：下述所列的所有常量，仅允许被细化模型访问：时、分、日、月和年是五个在被与其相关的功能所调用之前需要填入元素的集合。这五个集合只允许填入符合逻辑的值（例如：一小时的值要介于00-23，一分钟的值介于00-59，一天的值介于00-31）。将其余常量bill_paid，share_paid，joining_group 和leave_group这几个功能以日、月和年划分开，将这些信息作为数字来处理，从而避免去新建一个D A T E类，并且可以对这些数值进行比较。当与b ill_pa i d功能相关联时，需要进一步以时间的时、分来细化（如图3）。

图3：细化-常量Figure 3:Refinement-Invariants

2.2 细化Events

使用上述环境、变量和常量来表达对应关系并对每个细化需求（event）建模。

细化需求（1）：添加成员支付其账单份额的日期和时间

成员支付账单份额发生在以下三个events中：Members_pay_bill，Member_pays_initially和 Members_repay_bill。从上述第一条细化需求可得出，每当有成员支付其账单份额时，就需要添加发生的时间和日期。条件 6（@gr d6）、7（@gr d7）、10（@gr d10）、11（@grd11）和12（@grd12）用于确保时间和日期以正确的格式添加。条件 8（@gr d8）和 9（@gr d9）检查确保要添加的小时和分钟还未存在于当前集合share_paid_hour和share_paid_minute中。条件13（@gr d13）、14（@gr d14）和 15（@gr d15）检查添加日期是否已经存在于集合share_paid_day，share_paid_month和share_paid_year中。Events中发生的的所有行为（@act）就是将日期，时间和该成员支付的份额数值一起添加入正确合适的集合中。Members_pay_bill，Member_pays_initially 和 Members_repay_bill三个集合中的条件行为都相同，唯一的区别在于Members_repay_bill中行为的编号不同，故均以图4为代表。

细化需求（2）：添加账单全部付清的日期和时间

图4：细化-成员支付份额Figure 4:Refinement-Members pay his share

当账单全部付清后，会从待付账单集合中移出。据第二条细化需求的要求，账单付清时需要添加日期和时间。条件 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）均为将日期，时间和相应的已付清账单的数值一起添加进恰当的集合中（如图5）。

图5：细化-移出付清账单Figure 5:Refinement-Remove fully settled bill

细化需求（3）：添加成员加入小组的起始日期和退出小组的结束日期，当且仅当成员还是小组成员时，列出在其加入的每个小组内的应付账单份额。

为达到成员能够看到自己所加入的每个小组中应支付的账单份额的目的，需要在适当的集合中添加该成员加入每一个小组的日期，以及该成员退出每个小组的日期。Add Member Group中条件4（@gr d4）、5（@gr d5）和 6（@gr d6）检查确保试图添加的日期格式正确。条件 7（@gr d7）、8（@gr d8）和 9（@gr d9）检查需要添加的日期是否已经存在于集合join_group_day，join_group_month 和 join_group_year中。所有行为（@act）均是将日期与对应的该成员加入的小组添加到适当的集合中（见图6）。

Remove Member Group中的所有行为（@act）和条件（@grd）都类似于Add Member Group，区别仅在于与它相关联的日期不是join_group的日期，而是leave_group的日期。当某成员退出小组时，意味着该成员不再是小组的成员，那么需将其的join_group日期删除（见图6）。

图6：细化-成员加入/退出小组Figure 6:Refinement-Add/Remove amemberto/from a group

Deregister Member中所有条件（@grd）都与Remove Member Group完全相同。二者之间的区别仅在于活动（@act），当成员彻底从系统中注销时，需将join_group和l eave_group的日、月和年全部删除（见图7）。

图7：细化-成员注销Figure 7:Refinement-Deregister member

为每位成员和小组添加join_group和leave_group之后，需要列出某位成员所加入的每个小组中应付账单份额的数值，条件7（@grd7）、8（@grd8）和9（@gr d9）确保当前日期是正确的格式。条件10（@gr d10）确保该成员已经加入该小组，或者检查该成员是否今天退出了小组，也就是说某成员退出小组时，便不能够再去查看他在这组的账单份额的信息。条件11（@gr d11）确保当前日期在该成员加入该小组的日期之后，也就是说某成员只有在加入小组之后，才能够查看他在小组中的账单份额信息（如图 8）。

图8：细化-列出成员在每个小组的账单份额Figure 8:Refinement-Listallshares of a member at each of his group[4]

3 Pro-B规范化验证

与普通events相同，细化需求后的events也使用P ro-Banimator进行规范化验证。以下是规范验证的步骤流程。

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

图9：细化初始化前Figure 9:Before Refinement In itializatio

第二步：执行初始化event

所有模型中的变量在S tate窗口中为初始化默认值（如图 10）。

第三步：执行细化events

初始化之后，可运行的events 如下：Add_share，Add_initial_bill，RegisterMember，AddDate和CreateGroup。添加成员，创建小组并加入日期和时间（日，月，年，时，分）之后，AddMemberGroup，DeregisterMember，Add_initial_bill和add_share功能随即被激活。在抽象机制中， 若执行AddMemberGroup 功能，RemoveMemberGroup 和ListMemberGroup 随即被激活[5]。细化机器中，需要将join_date加入恰当的集合中，RemoveMemberGroup 中也要加入leave_date,同时DeregisterMember 中要将join_date 和leave_date都删除。

当账单已添加入Add_initial_bill 且Group 已加入到CreateGroup 时，Add_group_Bill 激活并将账单分配到小组中，随后Add_member_share 触发并将账单份额分配给组中成员。Add_member_share执行后，像在抽象机制中一样，支付账单的两种方式随即被激活。若小组中某成员支付账单全额，bill_date的时间的日期将被添加入相应的集合中。

图10：细化初始化Figure 10:Refinement-Initialization

账单全额付清时，该账单从小组中删除之前会重写bill_paid时间和日期集合，并且将该账单添加入paid_db集合中[6]。

全部执行的events的所有最终值如图11所示。

图11：执行细化Figure 11:Refinement-Execution

4 结论

通过账单分摊系统细化需求建模和验证的例子，可以看出E vent-B细化需求建模方法是当前扩展系统功能最为简便高效的方法，弥补了传统系统建模方法的缺陷。众所周知，软件危机是当前软件工程所面临的巨大危机，而解决这一危机的公认的有效方法是实现软件复用。软件复用的途径有很多，例如基于构件的开发方法。若能降低扩展系统功能的难度以及消耗，无疑会增强软件复用度。