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

摘要

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