event-B

第一章

介绍

在过去的30年，软件开发的许多领域引入并采用了形式化方法。近年来，软件工业使用VDM，Z，ASM，B和Event-B.然而这个领域的研究还在继续；尝试改进这些方法或获得益处。连接需求，详细说明和实现的工作还在继续。

1.1 背景和动机

面临Hoare 和Misra在【72】中提出的验证软件挑战，我们陈述了理论，工具和实验是形式化验证方向的三个主要挑战性研究方面。现在，许多先进的理论和有用的工具已经开发，并被软件社区采用。另外，现代机器的性能（与过去几年相比）足以进行形式化推理（定理证明，模型检验）所需的高级运算。实验很重要，并且这个学科仍然需要实验推动形式化方法并使得形式化方法更多的被软件工业采用的科学进程。Hoare和Misra说，进行实验应该用存在的工具和理论，与实际系统的选定领域,特别是那些担心安全问题的系统。实验有助于理解理论和工具的强弱方面，提供科学证据，支持理论和工具分析，鼓励其他研究者投入到未来更有效的研究中。

Event-B[4]是扩展了B方法【1】的形式化方法。它用于归约，验证复杂系统。包括并发和通信系统【31】。支持Event-B的工具由Rodin平台提供【6，5】.这个工具基于Eclipse【57】
，提供可扩展归约验证环境。

基于 flash 的文件系统是由Joshi 和 Holzmann【85】提出的挑战性系统。这个文件系统有吸引力的原因如下：首先，文件系统很复杂，尽管只是操作系统的一部分。例如，如何处理执行文件或flash操作时发生的错误？如何应对容错，当flash指令失效。如何确保并发访问的可靠性。更重要的是，正确性安全性对文件系统而言非常重要，因为存储在机器上的重要数据是由文件系统管理的。另外，大多数现在的文件系统有一个定义好的基于POSIX标准的接口【85】。然而，虽然设计文件系统使用的基本的数据结构和算法容易理解，文件系统仍然有bug。这些使用户和企业面临一个严重的问题。以美国国家航空和宇宙航行局（National Aeronautics and Space Administration）为例，管理flah内存卡（用于空间任务）的软件出现了意外。这可以引起突然的功率损耗和重启【76】。

研究文件系统需要强调的三个问题是功能需求，底层硬件，容错【117】.flash 内存是实现文件系统的诱人选择，因为flash内存没有移动部件，耗电小，容易获得。最近，flash成为飞行器上采用的主流非易失存储【85】。

1.2 研究方向和目标

方向：正如前面提到的，实验是形式化方法领域的重要研究途径。因此，用形式化方法和工具进行实验选为我们的研究方向。我们的工作重点在用E-B和Rodin平台进行实验。实验的目标是形式化地开发和实现基于flash的文件系统。在工作中，为了评价和比较，强调了许多建模技术或风格。一系列功能需求-影响树结构的操作，读写操作-作为系统的一部分，要对这些功能进行建模，验证和实现。三个重要问题：容错，并发，wear-levelling process。

研究成果:研究目标是以五种形式生成科学证明：

• 基于flash的文件系统的证明模型由归约，提精，证明组成。我们的模型包含三个问题：容错，并发，wear-levelling。其他相关工作中没有并发文件操作（读写）。另外，我们使用的文件系统的结构和特点与其他的文件系统也有区别。例如，我们用父结构代替名字路径，把文件系统表示为一个树结构。这些工作造成了重大的挑战【85】。（比较的具体细节见7.3）
  

• 调查比较了多种技术，选择合适的作为开发。增量方法选为我们的主要策略。在建模，证明文件系统（7章）的其他相关工作中没有使用这个方法。我们遵循着一个强大的系统的改进方法,组织细化过程，这个过错将是有益于其他研究者和实践者。我们的工作涵盖了完整的形式化开发（抽象归约，提精，证明和实现）。显存的形式化建模工作通常以为实现的模型结束。我们认为这有助于学习形式化方法和实现我们研究的人。
• 系统化的转换E-B到java代码实现。目标是提供系统化的转换规则，表明通过实施我们提出的规则，可以转换我们的模型。我们的转换规则定义了从E-B到java代码的直接转换，与其他的不同。如，Edmands et al【49】提供了一种工具用于表现类java模型，可以转换逞E-B模型用于形式化证明，也可以转换成java代码作为实现。（相关工作在8.4）
• 评估用于归约的方法和工具。我们的实验目的是评估E-B和Rodin工具，通过评价实验结果如证明数据，实现（是否最终结果满足），与其他方法和工具相比工具的功能。本文提出的评估展现了E-B和Rodin的优缺点，利于语言和工具的进一步改进。例如，为语言和工具增加那些部分使得它们更有用更利于使用。
• 建模，提精，证明规则。这些的目的在于提供新的证据，有利于形式化开发者，进一步研究，软件工业-模型技术，风格，形式化归约的样式。例如，特定的问题领域适合采用哪种形式化风格？现存的理论和工具可以达到什么效果。

1.3 简介方法和结果

用E-B和Rodin进行实验。基于flash的文件系统作为研究案例。增量提精作为我们的策略开发基于flash的文件系统模型。提精用于两个不同的方向，水平或特点增加和垂直提精或结构提精【27】.水平提精关注引入新的需求或特色，这些需求没有出现在初始模型中或推迟到其他提精阶段。在每个提精阶段，增加额外的状态变量和相关的事件包含引入的特点。增加新的属性逐渐扩大系统模型。另一方面，结构化提精的目标是用每个提精阶段的设计细节到实现取代抽象结构。这种提精可能涉及数据提精，事件分解和机制分解。

在开发中，用关注树结构操作的初始模型开始。之后，水平提精通过引入新的特点来扩大模型。之后，结构化提精关联抽象文件系统与flash需求。在这个阶段使用事件分解把原子事件（文件读，写）分解成子事件，为了关联flash接口层提供接口（页读，页编程）。然后，机制分解把文件系统机制分解成两个子机制（代表文件系统层和flash接口层），文件系统机制被flash需求代替了。此时，我们有两个子机制，可以分别进一步提精。在我们的工作中，进一步提精关注的是用flash需求覆盖其他flash特点和wear-levelling process。

我们的开发涵盖了三个主要问题（容错，并发，wear-levelling技术）。我们有两个主要的E-B模型。一个代表文件系统层，另一个代表flash接口层。flash接口层模型提供了到文件系统层的接口（页读，页编程）。wear-evelling技术延长flash设备的寿命，在这个模型中指定。文件系统模型描述了容错，可能发生在读写文件时。模型能够处理文件并发读写操作。flash接口模型能处理并发页读，编程和块擦除事件，错误。

定理提供了验证模型的策略。5，6章的开发，1.69个POs（proof Obligatins）由Rodin自动生成。671个POs由文件系统生成，398个POs由flash接口层生成。Most of them,94% (of the file system model)
and 100% (of the flash interface model),were discharged automatically (i.e. in total
1028 of 1069 POs (96%) were proved automatically). The rest,41 POs,were proved
interactively using the Rodin tool.
基于建模和证明的经验，我们提供了一些可供开发者学习的有用指导。指导被分成三类：建模，提精，证明。我们研究并提出把E-B模型转换成java代码的系统化转换规则。转换规则分成两部分：类构造，事件转换。然而，将来的工作是自动化应用这些规则。最后，我们依照归约和提出的转换规则实现了一个flash文件系统原型。实现包含两部分：文件系统层，flash接口层。我们模拟了部分flash接口层代替使用真正的flash，因为我们想模拟错误，测试模型是否能够处理这些错误。

1.4 章节纲要

在第二章，我们概述了一些现存的形式化方法以及它们对软件工程的重要性。第三章详述E-B和Rodin平台。在4，5，6章，案例研究工作-树结构文件系统和flash内存-说明如何用E-B和Rodin归约，提精系统模型。关于flash文件系统的相关工作在第七章讨论，比较。把E-B模型转换成java代码的系统化转换规则在第八章提出。flash文件系统的实现在第九章进行概述。建模，提精，证明指导在第十章讨论。最后，结论，对E-B和Rodin的评估和进一步的工作位于第十一章。

第二章

形式化方法

2.1介绍

这章的目的是概述形式化方法，技术和用于归约验证的工具的概况。这章以在2.2部分给出形式化方法的定义开始。第二，形式化方法对软件工程的重要性在2.3进行概述。第三，用现存的形式化方法和工具进行归约，验证在2.4给出。这部分，选择Z【20】，B【1】和VDM【84】为例子概述，比较形式化机制。选择它们的愿意：（1）它们是基于状态的方法，这种方法E-B的重要方法（2）它们是软件工业近些年使用的方法，然而近年也有使用其他形式化方法，如ASM【18】，Alloy【81】，这里我们不做解释。其他形式化机制例如时序逻辑，进程代数和行为系统在2.5节简述。最后，2.6节给出提精技术。

注意：为了让读者容易跟得上，E-B-我们开发使用的方法-将在第三章单独列出。

2.2形式化方法

形式化方法可以定义为用于归约，验证，推理软硬件系统的基于数学的技术【1，32，84】。形式化方法致力于用精确的文档向用户和开发者解释软件系统，这个文档以合适的抽象级构造呈现【83】。另外，形式化方法的目标是提供用户一些机制验证模型，如自动证明和模型验证。

因为用数学符号表示系统，所以用形式化方法表示的模型是可以用数学过程验证的良好数学逻辑结构状态。更重要的是，形式化方法的价值在于为用户（设计者，开发者）提供了为系统构造精确模型的方法，系统在之后会被实现。模型不是系统，是真实系统的抽象表示，在还没用系统的时候，就可以按照个人的想法推理验证系统【1】。这意味着不可以测试或执行模型来验证模型是否正常工作，是否拥有满足我们需求的属性。同样地，我们不可以使用构建模型内的任何空间。因此，推推导模型是分析模型的有效方法【6】。形式化归约语言支持系统功能表示。相应地，编程语言用于实现。虽然功能编程语言例如ML（Meta Language）【106，69】，Haskell【77，79】，和Scheme【55】更像归约语言因为它们描述了预期的结果，但是编程语言是可执行的【20】。

2.3 为什么形式化方法对于软件工程很重要

接下来的理由总结自Bowen【20】和Holloway【73】，说明形式化方法对软件开发的重要性。

正如之前提到的，形式化归约是结构良好的数学形态。因为它的精确行，即使这样的归约与非形式化的需求相比是无效的-例如，归约不是客户期望的-，找到哪里错误以及为什么错误是很容易的【20】。例如，在开发过程中发现错误时，我们可以查看归约组件如常量，preconditions ，proof obligations 检查它们是否满足需求或修改它们。相应地，非形式化需求是模糊的，很难发现改正错误。另外，用数学符号增加了对系统的理解，尤其是在设计阶段初期。它能够帮助设计者组织思路，使模型更加清晰，简单，容易理解【20】。更重要的是，形式化推导一个系统可能是通过陈述，证明系统相关的定理实现的。这些提供了一种机制，检查系统是否按照我们的期望运行。形式化方法也帮助开发者在系统实现前推导系统的操作【20】.例如，可以检查每个操作的前提条件是否满足需求，用手动查看或用模型检查和动作的工具查看。

设计错误是软件出错的主要原因。因为，为了确保软件正确运行，必需用一些方法处理设计错误。即使有不同的方法处理设计错误如测试，设计多样性，错误避免，可以减少设计错误的合适方法是形式化方法【73】.小系统或低可靠性系统可以用测试表示系统是否满足需求。然而，高集成的软件系统，测试将需要比可接受时间更多的时间来进行。更重要的是，基于测试的方法不能包含测试用例之外的情况。也就是，当系统执行测试用例之外的情况时，可能发生错误。因此，对于那些系统，基于测试的方法不充分。

如【20】陈述的，用形式化方法表示的精确需求容易实行直到实现阶段。可以减少设计中的错误。因此，当错误可以在设计阶段发现，修改时，开发周期内的交换就会减少。

另一点是，开发成本非常关键。如果在设计阶段发现错误，在设计阶段修改错误的成本远小于测试阶段发现错误。

2.4 现存的建模语言

这节将按顺序罗列现存的一些归约语言，Z，VDM，B。这节的结束部分将对它们进行比较。

2.4.1 Z 标记法

Z标记法【20】是形式化建模语言用于描述，推导计算机化系统。目标是提供系统的精确归约和系统行为形式化证明。最初由Jean-Raymond Abrial在1970年末引入，后来被Oxford 大学的编程研究小组的成员开发【20】。

Bowen【20】声明所有用Z标记表示的表达式都是基于集合理论，lambda演算，一阶谓词逻辑内的标准数学符号。Z包含一个标准化的数学函数列表和常用在归约呢的谓词。

只使用数学的问题是大归约通常变得不可管理和难以理解。因此，在Z中引入模式标记辅助归约的构造。这提供了一个框架，框架用于用类似数学操作符的模式操作符表示的模式文本组合【20】。

Z中抽象归约的概念用来表示系统做什么而不是如何做。它被设计成富有表现性，容易推导而不是计算机可执行性。

2.4.2 Z结构和例子

用框标记表示的模式辅助Z归约的构造。模式用于描述归约的两个主要部分：状态域和操作【20】.

表示在下面的状态空间模式分成两部分。第一部分用于定义状态变量（x1,x2,...,xn），第二部分表示那些变量中的常量。

StateSpace
x1 : S1
x2 : S2
...
xn : Sn

Inv (x 1,xn)
下面是Hughes介绍的虚拟文件系统模型的Z模式的例子【78】。下面的模式是FileSysState的状态空间，由命名为objects的对象集合和函数parent组成。parent函数是映射OBJ到OBJ的特殊函数，OBJ是集合类型。两个常量，desktop和trash。

FileSysState
objects : P OBJ
loc : OBJ? → OBJ

desktop ∈ objects trash ∈ objects dom parent = objects ? desktop ran parent ? objects parent(trash) = desktop (parent ?1 )? ({desktop}) = objects