基于Event-B方法的需求建模及验证

Event-B Modelling and Specification Verification

Event-B是国外新兴的一种通过形式化方法,主要用于对系统功能性需求建模并验证,在Rodin工具集中,通过给出环境、变量、常量和相关事件,对每一个抽象需求建模。其后,使用Pro-B animator进行验证。它通过逻辑分析产生验证规约并且自动抛除无关紧要的验证规约来取代传统的编译,解决了传统的软件工程过程中系统分析与设计阶段非形式化方法带来的低效率,错误率高,不易纠错,不灵活,编码复杂以及常常不够符合实际的缺陷。以账单分摊系统为例,详细描述了Event-B方法的需求建模和规范化验证的思路和过程方法。

Event-B is a formal method for modelling and verifying functional requirements of systems well-used among foreign countries.Each abstract requirement is modelled in the Rodin tool set,by providing the context,variables,invariant and relevant events for it.Then,those requirements can be verified using the Pro-B animator.It focus on proof obligation generation and automatically discharging trivial proof obligations by logical analyse instead of traditional compiling.Differing from inefficient,high error rate,hard to achieve error correction,stiff,complicated and impractical traditional informal methods.Event-B provides the easy way to replace compiling which confuses software engineers and time-consuming.The billsplit system is used as an example to demonstrate the thoughts,methods and process during Event-B modelling and specification verification in detail.