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

彭 寒,张晓丽,刘洲洲,曹国震,景月娟,王 瑾,李添锐

1(西安航空学院 计算机学院,西安 710077)

2(西安石油大学 计算机学院,西安 710065)

1 引言

随着物联网、云计算、信息物理融合系统时代的到来,“软件定义”已成为当前计算机科学以及软件学科的研究热点.软件的泛在化导致软件系统的规模日渐庞大,复杂度不断攀升,让软件设计和验证的难度不断增长.为应对软件设计、开发和验证中的复杂性,国内外研究团队不断提出新的、先进的软件设计与验证理论来提升软件开发效率、保证软件制品的安全性和可靠性.软件工程的形式化方法[1]是目前最有前景的软件开发方法之一.在形式化方法的支持下,研究人员能够使用严格的数学模型来描述系统的需求,并验证给定的系统或系统模型是否满足所要求的行为属性[2].虽然形式化方法已经被证明是保证系统的正确性和一致性的良好方法,但是其在软件工程中的应用一直无法大范围推广.其原因在于形式化方法的学习成本较高、可理解性差,且形式化模型在结构化、模块化和复用性方面存在一定局限.

Abrial 等发明的Event-B[3]是目前最贴近软件工程的一种形式化语言,其逐步精化的思想和自动代码生成的能力,不仅保证了模型的正确性和一致性,同时又能对软件开发的全寿命周期提供良好的支持.Event-B 方法已经成为支持软件工程形式化的主要方法之一.

本文首先对已有的基于Event-B的软件工程形式化方法……