Event-B 形式化建模介绍

Event-B模型构建方法

【first page】

首先介绍一下什么是Event-B，Event-B方法是由欧洲科学院院士阿布瑞尔发明的一种形式化建模方法，这个方法基于一阶逻辑和集合理论，可以进行系统层次的建模和分析。那么Event-B建模方法大致有这么几个主要环节——需求，建模，精化以及证明。

传统的软件开发过程中，软件需求往往不是很精确，而Event-B建模过程中的需求设计是十分严格和规范的，哪怕它也是用非形式化语言来表示的，由于这些语言往往有着很强的逻辑关系，可以说是对整个系统进行了十分规范和准确的无歧义的描述，这个在之后的例子中可以看到。

其次就是建模过程，当然在建模之前我们还需要设计一个精化的策略，这样能够帮助我们有条不紊地实现后续的精化。

而精化的过程能够让我们建立的模型越来越具体，越来越逼近我们最终想要的，直到最后满足所有的需求。

建模过程中我们需要借助Event-B的开发工具Rodin平台来证明模型的正确性。我们需要保证在每一个事件中的不变式是能维持的、或者能够证明模型中是不会出现死锁的。这样才能确保最后的精化模型是安全可靠的。

【new page】

Event-B作为一个建模方法，那它的模型是怎样的一个结构呢？可以看下这幅图，Event-B的模型包括了机器和环境。那么机器包括了变量、不变式、定理、事件等建模元素，环境包括了集合、常量、公理、定理等建模元素。这些元素都是用集合、一阶逻辑来表示的。也就是说，机器中包含了模型的动态元素，而在环境中包含了模型的静态元素。

那么对于一个模型而言，机器与环境之间存在着一些关系，如图所示，机器与机器之间会存在精化关系，环境与环境之间会存在延伸关系，而机器与环境之间又会存在可见关系。 【new page】

Rodin平台作为Event-B的建模开发环境，可以说，他让建模也有了编程的感觉，而Rodin中的证明器让我们对设计的模型进行debug调试成为了可能。

案例：内存管理模块建模

那么Event-B这套形式化方法具体是如何去构建一个复杂系统的呢，这里给大家展示一个例子，也就是用Event—B的方法对一个实时操作系统中的内存模块进行形式化的建模。这种建模方式往往对系统功能需求作出很严格的要求。这也是保证整个系统安全可靠的第一步。

【new page】

功能需求层

那么如何设计出这样的安全可靠的需求呢？就拿这个例子而言，我们需要对内存管理的需求分成这几个方面。一是内存和内存块的物理特性以及已被分配和释放的内存块的特点，二是分配和释放内存块的操作，三是实现管理空闲的内存块。那么具体怎样去描述这些方面的需求呢？

【new page】

例如内存需要满足什么要求。很显然，这个系统是管理着该操作系统的内存的，将此作为功能需求1；其次内存地址是一个有限的自然数区间，并且其实地址为0，将此作为系统的环境需求1。

对于块，也需要有类似的需求设计：一个块的内存是连续的，以及不会存在空的内存块。这些都是需要满足的环境需求。

【new page】

再例如，系统要求每一个块要么是已被占用，要么就是是空闲的。以及一个空闲块总是被占用的块包围。再看一个具体的释放内存块的操作需求，如果所要释放的块不是一个正在被占用的内存块，那么释放该内存块失败，否则就成功。

因此，通过这样的一种，对系统的环境和操作进行严格的需求定义，并将其放入一个表格中并标上序号的方式就可能得到一个相对来说更加安全与可靠的需求模型。而这就为接下来的整个可靠系统的设计带来了方便。

软件设计层

【new page】

对于内存管理模块的软件设计模型，重点就是利用之前提到的精化策略。那么具体是怎样一个过程呢？既然是一个策略，其实主要就是处理一件事，这些需求该怎样在模型中一步一步得到满足。例如内存管理这个例子，就是需要定义内存的静态的状态和基本的操作。那么设计精化策略时就需要在初始状态模型到第五次精化模型期间定义并精化基本的操作。而后在第六到第七次精化中实现分配内存和释放内存的具体功能，也就是调用之前模型里的操作。在第八到第十次精化中再加入搜索算法得到最后的精化模型。

【new page】

我们可以看这张表，它将每一次精化所满足的需求呈现了出来，通过之前提到过的，增加不变式，引入新事件等方法一步一步对初始模型进行精化，直到满足了所有的需求。从而确保了整个模块的建模过程是一个越来越逼近于完整的系统需求的过程，软件设计与需求设计的一致性因此得到了满足。

软件实现层

【new page】

整个建模过程实在Rodin平台上进行的，刚才也大致了解了这个工具，基于eclipse使得建模也有了编程的味道。在该平台上建立好模型后它会对不变式进行自动证明，对于不能自动证明的不变式，我们只需要在证明器中引导它证明就行。

【new page】

证明完全的模型就可以通过自动代码生成工具生成部分代码，无法自动生成的需要人工实现。

总结

【new page】

因此，在操作系统内存模块建模的案例中可以看出Event-B方法在可信软件开发中的优势：

在可信系统功能层上进行严格的需求规范，通过得到功能性需求和环境需求并进行编号，能够详细地描述一个复杂系统的需求。

在软件设计层上，设计精化策略、然后用严谨的数学符号建立模型并逐步精化、证明就可以得到一个安全可靠的系统模型

最后在软件实现层可以通过Event-B进行模型仿真或者通过一些工具生成部分代码。

通过这套建模理论就可以大大提高开发的模型或者系统的安全性、可靠性。