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

Event-B Refinement Modelling and Specification Verification

Event-B通过为每个event添加环境、变量及常量等限制条件,从而细化及快速扩展系统功能,避免数据冗余问题。以账单分摊系统为例,通过添加成员支付账单、账单全部付清及成员加入和退出小组的日期及时间等三点细分需求,详细描述了使用Rodin工具集细化需求建模及通过Pro-B animator进行规范性验证的方法和过程。

Traditional system modelling is determined, which means it can’t add more functions easily.But Event-B, which differs from most system modellings, can be defined, which means to add some variables, invariants and context to achieve more functions(extend system functions).With refinement, it can be easier to correct and fulfill the event instead of building a lot of new events,avoiding causing data redundant. In billsplit system, refined requirements modelling by using Rodin tool set and the methods and procedures of refinement specification verification are demonstrated in detail, by adding three refined requirements: add date and time to a member’s share when he pays it, add date and time to a bill when it is fully settled, add start date when a member joins a group and an end date when he leaves.