Event-B 形式化建模语言概述

软件工程中的形式化方法

形式化方法是基于严格数学基础，对计算机软（硬）件系统进行形式规约、开发和验证的技术。其中，形式规约使用形式语言构建所开发的软件系统的规约，它们对应于软件生命周期不同阶段的制品，刻画系统不同抽象层次的模型和性质，例如需求模型、设计模型甚至代码和代码的执行模型等。形式验证是证明不同形式规约之间的逻辑关系，这些逻辑关系反映了在软件开发不同阶段软件制品之间的需要满足的各类正确性需求。例如，形式验证给出“系统设计模型满足若干特定性质”的证明构造.在形式规约和验证的基础上，形式化开发主要是构造、证明形式规约之间的等价转换和精化关系，以系统的形式模型为指导，逐步精化，开发出满足需要的系统，也称为构造即正确（correct by construction）的开发。

形式化方法与其他软件开发方法的主要区别在于：其描述软件及其性质的语言是无歧义的，构造和验证软件的方法是严格的。在软件工程中，形式化方法提供了工程化系统设计的一种比较透彻的思维方式，可以很好地支持抽象模型建立、系统精化、模型和证明重用；形式化开发过程具有很好的可重复性，相应的软件制品模型也具有较强的可分析性和可验证性。因而，形式化方法可以有效地提高和保障系统的可信性。

综上所述，形式化方法是由形式规约语言（包括形式语义与模型理论）、形式规约（包括精化与综合）、形式验证、形式化工具等形成的一个整体。其中，形式规约语言是基础，形式化方法中，软件制品是规约语言编写/变换的形式规约；形式验证是保证开发正确性的途径，形式语义与模型理论是联接形式规约和形式验证的数学纽带；形式化工具是系统设计和开发中高效使用形式化方法的需要和实践。

Event-B 基本原理

Event-B 是一种用于系统级别的建模和分析的形式化方法。它在 B 方法基础上发展出来的、基于状态和事件的形式化系统，并支持基于精化的模型转换和性质证明。

Machine (抽象机) 和 Context (上下文)

用 Event-B 做形式化开发，最基本的概念就是模型。一个模型包含了一个离散迁移系统的完整数学开发，它由分属两个类别的一些组件构成，这两个类别分别称为抽象机和上下文。抽象机包含模型的动态部分，也就是变量、不变式、定理、变动式和事件；而上下文包含模型的静态部分，包括载体集合、常量、公理和定理。

使用 Event-B 建模时，首先建立一个模型 (Model)，一个完整的 Event-B 模型应该包括上下文 (Context) 和抽象机 (Machine)：

• Context（上下文）：上下文主要定义常量，这些常量可以是数值或者数据集合。

  • Variable：变量定义了状态变量，我的理解是全局的变量
  • Invariant：不变式定义了相应 Variable 的类型
  • Theorems：定理定义了相应 Variable 的行为
  • Events：事件定义了能使状态变量改变的事件，其中包括初始化
  • Variant：变动式相对于 Variable 来说，则是 Events 中临时变量，作用域比 Variable 小

• Machine（抽象机）：抽象机主要定义动态的行为，包括状态以及状态属性，还有事件模型的建立都在 Machine 模型里建立。

  • Sets：载体集合是数据集合
  • Constants：常量是定义的一些常量
  • Axioms：公理描述了不能从其他公理派生出来的属性
  • Theorems：定理描述了可以由公理导出的性质

精化和扩充（Refine and Extend）

一个项目中可以存在多个 Machine 和 Context，但它们不能是独立的，这也从侧面解释了“Event-B 支持逐步精化地建立系统模型”。抽象机和上下文之间存在多种关系：一个抽象机可以被另一个抽象机“精化”，一个上下文可以被另一个上下文“扩充”，一个抽象机可以“观看”一个或几个上下文，下图描绘了机器和上下文之间的关系。

精化是增加系统的功能、增加细节、改变状态模型。精化一个自动机过程中，可能需要增加新的变量和新的事件。一般一个模型需要进行多次精化才能符合要求。即 Machine 在精化中越来越复杂，越来越细致。Context 也越来越庞大。抽象机和上下文之间的可见性遵循下面的规则：

• 一个抽象机可以显式地观看若干上下文（也可以不观看上下文）.
• 一个上下文可以显式地扩充若干上下文（也可以不扩充任何上下文）.
• 上下文扩充的概念具有传递性：当上下文 C1 显式地扩充另一上下文 C2 时，它也隐式地扩充了那些被 C2 扩充的上下文.
• 当上下文 C1 扩充上下文 C2 时，C2 的集合和常量都能被 C1 使用.
• 一个抽象机显式观看某个上下文时，也就隐含地观看所有被其扩充的上下文.
• 抽象机 M 观看上下文 C，就意味着 C 的所有集合和常量都能在 M 里使用.
• 把精化和扩充关系放一起，不允许出现任何循环.
• 一个抽象机只能精化至多另一个抽象机.
• 一个抽象机显式或隐式观看的上下文必须不小于它所精化的那一个抽象机.

Event-B 方法支持构造不同精化层次的形式化模型，能使每一个抽象机都保持适当的规模。抽象机必须保持不变式和联结不变式（Gluing Invariants，联系具有精化关系的两个抽象机的不变式）。一个抽象机最多只能精化一个抽象机，通过引入新的变量、新的不变式和新的事件精化抽象机中的状态或事件。抽象机之间的精化关系是指对应事件之间具有精化关系，事件之间的精化关系是指对应事件的卫式条件满足卫式条件加强、动作满足模拟关系。

证明义务（Proof Obligation）

证明义务规则定义定义了“对一个 Event-B 模型必须证明些什么”。证明义务（proof obligation）并不是为了得到某些信息而进行的操作，它并不是必须的。它的作用只是确定建立的模型是否符合原始需求以及内部需求。

Rodin 平台中有一个称为证明义务生成器的工具，它对上下文和抽象机的正文做一些静态检查，自动确定要证明的东西。这些相继式被送给证明器，在那里完成自动的或者交互式的证明。证明义务规则包括：

规则名称	描述
不变式保持证明义务规则 INV	保证机器里的每一条不变式被每个事件保持
可行性证明义务规则 FIS	保证非确定性动作的可行性
卫加强证明义务规则 GRD	保证一个具体事件的具体卫强与对应的抽象事件的抽象卫。这样就能保证当具体事件被使能时，抽象事件也能被使能
归并证明义务规则 MRG	保证当一个具体事件归并了两个抽象事件时，它的卫应强于那两个抽象事件卫的析取
模拟证明义务规则 SIM	保证在一个精华里，每一个抽象事件的每个动作，在相应精华里都得到了正确的模拟
数值变动式证明义务规则 NAT	保证在每个收敛的或者预期事件的卫条件下，我们提出的变动式确实是有自然数值
有穷集变动式证明义务规则 FIN	保证在每个收敛的或者预期事件的卫条件下，我们提出的集合变动式确实是一个有穷集
变动量证明义务规则 VAR	保证每一个收敛事件都能使我们提出的数值变动式或者有穷集变动式减小。保证了每一个预期事件不会增大我们提出的数值变动式或有穷集变动式
非确定性见证证明义务规则 WFIS	保证在一个具体事件的见证谓词中提出的每个见证都存在
定理证明义务规则 THM	保证所提出的上下文或及其定理是可证的。定理的重要性在于有可能简化证明
良好证明义务规则 WD	保证每个有可能病态定义的公理、定理、不变式、卫、动作、变动式或者见证都确实是良好定义的

推理规则

相继式

相继式用来表示证明的目标，具有如下结构：
$$
H \vdash G
$$

• $H$ 是一个有穷的谓词集合，称为假设 (hypothes)，可以为空集
• $G$ 是一个谓词，称为目标 (goal)
• 符号 $\vdash$ 表示推导出 (entail)。注意这个符号不能理解成蕴含，相继式不是谓词，如果 $\vdash$ 换成 $\Rightarrow$ 那就成了谓词了。

这里还要特别区分一下 $\vdash$（推导出、满足）和 $\Rightarrow$（蕴含）的语义。$a \Rightarrow b$ 是一个谓词（如果 $a$ 和 $b$ 都有具体的意义那就是一个命题公式），这是可真可假的。但是 $a \vdash b$ 没有真假的概念，就是表述这样一件事。

基本推理规则

推理规则是基于相继式的，是上下两部分的推理结构：
$$
\frac{A}{C}
$$
其中 $A$ 是一个相继式的集合，可以为空集，表示推理的**前件 (antecedents)。$C$ 是一条相继式，表示推论 (consequnet)**。推理规则$\frac{A}{C}$ 表示如果 $A$ 中的所有相继式都能得到证明，则可以得到相继式 $C$ 的证明。

• 正向推理：证明 $A$ 中的每一条，将附属得到 $C$ 的证明。
• 反向推理：如果要证明 $C$，一个充分（但不必要）的办法就是证明 $A$ 中的每一条。

这只是在说期望通过推理得到结果的两种不同的“认知过程”，Event-B 里更多使用反向推理。

规则	公式
HYP	$\Large \frac{}{\mathbf{H}, \ \mathbf{P} \ \vdash \ \mathbf{P}}$
MON	$\Large \frac{\mathbf{H1} \ \vdash \ \mathbf{G}}{\mathbf{H1}, \ \mathbf{H2} \ \vdash \ \mathbf{G}}$
CUT	$\Large \frac{\mathbf{H} \ \vdash \mathbf{P} \quad \mathbf{H}, \ \mathbf{P} \ \vdash \ \mathbf{Q}}{\mathbf{H} \ \vdash \ \mathbf{Q}}$

参考文章：https://blog.csdn.net/SHU15121856/article/details/105925314

适用于命题逻辑语言下的推理规则

命题逻辑语言

$$
\begin{aligned}
Predicate := & \bot \
& \top \
& \lnot Predicate \
& Predicate \ \land \ Predicate \
& Predicate \ \lor \ Predicate \
& Predicate \ \Rightarrow \ Predicate \
& Predicate \ \Leftrightarrow \ Predicate
\end{aligned}
$$

为避免二义性，结合时先 $\neg$ 再 $\wedge$、$\vee$ 最后 $\Rightarrow$、$\Leftrightarrow$。并且 $\wedge$ 和 $\vee$ 是左结合的，而 $\Rightarrow$ 和 $\Leftrightarrow$ 是不结合的（连续使用必须加括号）。

推理规则

规则	公式
FALSE_L	$\Large \frac{}{\mathbf{H}, \ \bot \ \vdash \ \mathbf{P}}$
FALSR_R	$\Large \frac{\mathbf{H} \ \vdash \ \mathbf{P} \quad \mathbf{H} \ \vdash \ \lnot \mathbf{P}}{\mathbf{H} \ \vdash \ \bot}$
NOT_L	$\Large \frac{\mathbf{H}, \ \lnot \mathbf{Q} \ \vdash \ \mathbf{P}}{\mathbf{H}, \ \lnot \mathbf{P} \ \vdash \ \mathbf{Q}}$
NOT_R	$\Large \frac{\mathbf{H}, \ \mathbf{P} \ \vdash \ \bot}{\mathbf{H} \ \vdash \ \lnot \mathbf{P}}$
AND_L	$\Large \frac{\mathbf{H}, \ \mathbf{P}, \ \mathbf{Q} \ \vdash \ \mathbf{R}}{\mathbf{H}, \ \mathbf{P} \land \mathbf{Q} \ \vdash \ \mathbf{R}}$
AND_R	$\Large \frac{\mathbf{H} \ \vdash \ \mathbf{P} \quad \mathbf{H} \ \vdash \ \mathbf{Q}}{\mathbf{H} \ \vdash \ \mathbf{P} \land \mathbf{Q}}$
OR_L	$\Large \frac{\mathbf{H}, \ \mathbf{P} \ \vdash \ \mathbf{R} \quad \mathbf{H}, \ \mathbf{Q} \ \vdash \ \mathbf{R}}{\mathbf{H}, \ \mathbf{P} \lor \mathbf{Q} \ \vdash \ \mathbf{R}}$
OR_R	$\Large \frac{\mathbf{H}, \ \lnot \mathbf{P} \ \vdash \ \mathbf{Q}}{\mathbf{H} \ \vdash \ \mathbf{P} \lor \mathbf{Q}}$
IMP_L	$\Large \frac{\mathbf{H}, \ \mathbf{P}, \ \mathbf{Q} \ \vdash \ \mathbf{R}}{\mathbf{H}, \ \mathbf{P}, \ \mathbf{P} \Rightarrow \mathbf{Q} \ \vdash \ \mathbf{R}}$
IMP_R	$\Large \frac{\mathbf{H}, \ \mathbf{P} \ \vdash \ \mathbf{Q}}{\mathbf{H} \ \vdash \ \mathbf{P} \Rightarrow \mathbf{Q}}$
P1	$\Large \frac{}{\ \vdash \ 0 \ \in \ \mathbb{N}}$
P2	$\Large \frac{}{\mathbf{n} \ \in \ \mathbb{N} \ \vdash \ \mathbf{n} +1 \ \in \ \mathbb{N}}$
P3	$\Large \frac{}{\mathbf{n} \ \in \ \mathbb{N} \ \vdash \ 0 \ \leqslant \ \mathbf{n}}$

注意这些推理规则的命名上有后缀 _L 和 _R，可以称为左规则和右规则（未必都只有一条，只是命题逻辑这里恰好左一条右一条）。左规则总是变换相继式的假设部分（$\vdash$ 左侧），右规则总是变换相继式的目标（$\vdash$ 右侧）。

参考资料

1. Modeling in Event-B: System and Software Engineering, J.R. Abrial (2010)
2. Rodin User’s Handbook
3. 王戟, 詹乃军, 冯新宇,等. 形式化方法概貌[J]. 软件学报, 2019, 30(001):33-61.
4. Event-B形式化方法