基于Event-B方法的需求建模及验证
作者：史逸轩
作者机构：忻州师范学院,山西忻州034000
来源：忻州师范学院学报
ISSN：1671-1491
年：2019
卷：035
期：002
页码：24-31
页数：8
中图分类：TP311.5
正文语种：chi
关键词：形式化方法;Event-B;Pro-B;Rodin;逻辑分析
摘要：Event-B是国外新兴的一种通过形式化方法,主要用于对系统功能性需求建模并验证,在Rodin工具集中,通过给出环境、变量、常量和相关事件,对每一个抽象需求建模.其后,使用Pro-Banimator进行验证.它通过逻辑分析产生验证规约并且自动抛除无关紧要的验证规约来取代传统的编译,解决了传统的软件工程过程中系统分析与设计阶段非形式化方法带来的低效率,错误率高,不易纠错,不灵活,编码复杂以及常常不够符合实际的缺陷.以账单分摊系统为例,详细描述了Event-B方法的需求建模和规范化验证的思路和过程方法.
本文来源：https://www.2haoxitong.net/k/doc/ee0aeee100d276a20029bd64783e0912a2167cc8.html
文档为doc格式