基于Event-B的软件工程形式化方法综述

Overview on Formal Methods of Software Engineering Based on Event-B

在当今泛在计算和软件定义的大趋势下,形式化方法逐步成为指导软件需求定义、分析软件设计方案、验证软件制品正确性的重要方法,渗透到软件工程的全寿命周期. Event-B作为一种"构造即正确"的方法,为软件工程形式化方法的应用提供了支撑.本文对现有的基于Event-B的软件工程形式化方法进行了分类阐述,主要分为Event-B控制结构、面向对象的Event-B、可重用的Event-B以及实时Event-B模型,并对各种Event-B模型对软件开发全寿命周期的支持进行了汇总,为软件工程形式化方法提供参考和借鉴.

In today’s general trend for ubiquitous computing and software definition, formal methods have gradually become an important way to guide the definition of software requirements, analyze software design schemes, and verify the correctness of software products, which penetrates the entire life cycle of software engineering. Event-B, as a "correct by construction" method, supports the application of formal methods in software engineering. This paper classifies and expounds on the existing formal methods in software engineering based on Event-B, which are mainly divided into EventB control structure, object-oriented Event-B, reusable Event-B, as well as real-time Event-B models. It also summarizes the support from various Event-B models for the whole life cycle of software development and provides references for the formal methods in software engineering.