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

作     者：彭寒 张晓丽 刘洲洲 曹国震 景月娟 王瑾 李添锐 PENG Han;ZHANG Xiao-Li;LIU Zhou-Zhou;CAO Guo-Zhen;JING Yue-Juan;WANG Jin;LI Tian-Rui

作者机构：西安航空学院计算机学院西安710077 西安石油大学计算机学院西安710065 

出 版 物：《计算机系统应用》 (Computer Systems & Applications)

年 卷 期：2021年第30卷第9期

页      面：12-23页

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：陕西省重点研发计划(2018GY-028,2020GY-084) 陕西省自然科学基金(2020JM-633) 陕西省教育厅科研计划(20JG014)。 

主　　题：软件工程 形式化方法 面向对象 可重用形式化模型 

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