Jean-Raymond Abrial是国际著名软件和软件理论专家，1938年生于法国，目前是瑞士苏黎世联邦理工学院教授（这所学校曾经有爱因斯坦、冯诺依曼等大师执教或学习，是欧洲最著名的学府之一，图灵奖获得者Niklaus Wirth教授工作于该大学的计算机科学系）。他是Z 语言和 B 方法的创建者，软件形式化开发领域的最主要奠基人之一。参与和指导了欧洲许多重要的关键性软件开发项目。他从20世纪70年代开始研究数据结构的程序的形式化规范问题，20世纪70年代后期在牛津大学程序设计研究组(PRG)访问期间完成了有关形式化规范语言的开创性工作。为了将形式化方法与软件开发更好地平滑衔接， J-R  abrial从20世纪80年代前期开始了B语言和方法的研究和开发。这一方法的目的是希望为整个软件开发过程提供坚实的数学基础。随着方法的发展和成熟， 其开发的 B 软件开发方法被欧洲等地区的许多重要企业和部门（如欧洲航天局、西门子、阿尔斯通等）用于轨道交通、高铁、航空、电站等重要领域的信号、控制、调度、自动驾驶等各种关键性系统的建模、验证和系统开发。近年领导和参与 B 方法后继的 Event-B 开发和应用的欧共体项目，其参与开发的 Event-B 公开免费工具 Rodin 已被全世界软件/硬件和其他领域的许多理论和实际工作者使用。

形式化方法的研究和应用已有30多年的历史。最早的产生是由Dijkstra和Hoare在程序验证方法的工作，以及Scott、Stratchery和其他学者在程序语义方法的工作基础上发展起来的。形式化技术已经成为计算机科学的一个重要分支和研究领域，其作用相当于传统工程设计（如计算流体动力学，CFD）在航空设计中的作用。

形式化方法通过形式化和规范化的数学理论，用描述“做什么”来取代“怎么做”，其基本思想是对系统建立一个数学模型，研究和提供一种基于数学的或形式语义的规格说明语言，用这种语言严格地描述说开发的软件模型，并由自动程序设计的加工模型来得到可执行的代码。

安全系统设计的关键是要根据系统安全的需求，设计和实现有安全控制的、清晰的、全面的理解和描述。根据对系统的安全性级别要求的高低，采用不同的开发方法。对于一个要求中等安全程度的系统而言，可以采用自然语言描述描述；而对于高安全等级的系统，则要采用形式方法来对精确的安全定义进行建模。在安全关键系统中，必须要采用数学模型、形式化描述和验证技术等。

形式化方法以数学为基础，其目标是建立精确的、无二义性的语义，对系统开发的各个阶段进行有效的描述，使系统的结构具有先天的合理性、正确性和良好的维护性，能较好地满足用户需求。形式化方法关注模型获取、模型验证和程序求精，具有数学精确性的形式化方法适合安全关键系统的设计和开发。

形式方法包含两个侧面：一是形式规约，二是设计验证。基于形式方法的方法学要求，首先必须精确说明软件片断的行为，并用形式规约语言进行书写，称此过程为形式规约过程；然后指明其实际实现是否满足该规约，称此过程为设计验证过程。设计验证技术主要包括定理证明（Theorem Proof）和模型检测( Model Checking)。软件规格包括需求规格、功能规格、性能规格和设计规格，其中软件需求规格从用户角度描述了对所需软件的各种需求，如功能需求和性能需求等，用以书写软件需求规格的语言称为需求规格语言。软件功能和性能规格通常基于抽象的数学模型给出了软件“做什么”的功能以及在速度和资源等方面的限制。软件设计规格则是从可执行的角度刻画了软件的数据结构和抽象算法。

美国国防部的“可信计算机系统的评价标准”中，从B级开始就要求形式化模型技术的应用，A1级更是要求了形式化的最高层描述和验证、以及对形式化的隐密通道进行分析等；此外，形式化技术对在系统和软件开发中的规范化、控制费用、减少设计错误、方便软件测试和维护等方面都有显著的效果。

形式化方法在铁路安全控制系统中应用的重要性已得到许多专家认可。Hansen对丹麦的铁路联锁系统，其中包括轨道拓扑逻辑的面向图形的表示和安全规范中的逻辑条件进行VDM建模。Wong和Monige分别用图形和逻辑对轨道拓扑逻辑进行形式化描述。法国的SACEM项目在巴黎地铁的车速控制软件开发生命周期中采取了形式化方法,使用B语言和方法跟单编码处理器相结合，取得了良好效果。Z语言在一些工业系统，尤其是安全关键系统中得到了广泛的应用。Jacky和Jonhnson介绍了基于Z语言的规格说明在安全关键系统中的应用。

自动饮料贩卖机的Z规格设计

形式化方法主要研究形式化规约和形式化验证。根据给定的目标软件系统的方式，形式化方法可以分为两类：①面向模型的方法。通过构造一个数学模型来说明系统的行为。②面向属性的方法。通过描述目标软件系统的各种属性来间接定义系统行为。传统的验证方法包括模拟(Simulation)和测试(Testing)，是通过实验的方法对系统进行查错。目前常用的形式验证方法主要可分为两类:演绎验证(Deductive Verification)和模型检测(Model Checking)。

形式化理论与方法的研究己经引起了轨道交通控制系统研究人员的极大关注，主要的关注点包括：① 在将非形式化的需求转换成形式化规约的过程中，二义性、需求的增量和矛盾较易发现；② 形式模型将导致层次化的半自动甚至是自动化的系统开发方法；③ 与通常的用例测试相比，形式化方法可以用数学的方法验证其正确性；④ 一个经过验证的子系统可以并入一个形式或非形式的大的系统中，这将增加系统符合规约的可信度；⑤ 使得开发者可以评估、比较各种不同的设计。

目前，国际上一共开发出了九十多种形式化语言，每种语言都是其自身的适应环境和特定条件。适合轨道交通信号系统安全设计模型的形式化语言不多，主要包括：Z语言、B语言、VDM以及OBJ等。

① B方法：在法国的SACEM项目中得到了充分的应用，并且其效果也是十分令人满意的。在该项目中采用了两个互补的技术来达到高安全等级，即B方法和单编码处理器(Coded Monoprocessor)。B方法用于软件的规划说明、设计和代码实现，确保源代码无错地实现所规格说明；单编码处理器确保在硬件故障或编译器出错的情况下的执行操作不产生任何危险。

B方法是由Jean-Raymond Abrial创造的。它覆盖了软件的整个开发周期，适用于大规模软件的开发。B方法以元集合理论和二值谓词逻辑为数学基础，其核心是证据，且必须论证B方法所描述的每一个特性，这为开发者提供了统一的形式化规范和代码。B方法是由模块组成的，模块给出了数据和在这些数据上的操作。模块进一步被分成：机器(Machine)、求精和实现，机器给出了模块的外部描述，仅仅说明用户对模块的需求是什么；求精给出了模块的内部描述，完全规范模块的行为。机器和求精是抽象的部件，它们的数据可以是集合或关系。实现是具体的，它直接将它们转化成典型的语言，数据结构是有限制的(整型、布尔型和数组)。

②Z语言是目前非常流行的一种形式规格说明语言，具有“状态一操作”风格。它是以一阶谓词逻辑和集合论作为形式语义基础，将函数、映射、关系等教学方法用于规格说明。Z借助于模式来表达系统结构，它提供了一种能独立于实现的、可推理的系统数学模型，具有精确、简洁、无二义性的优点，有利于保证程序的正确性，尤其适用于无法进行现场调试的高安全性系统的开发。Z最主要的结构是模式，一个模式由变量说明和谓词约束两部份组成，可用来描述系统状态和操作。Z语言利用模式和模式演算对软件系统的结构和行为特征进行抽象描述，其中状态模式对软件系统的结构特征进行抽象描述，而操作模式对软件系统的行为特征进行抽象描述。Z有模式匹配的符号，使用了具有强大功能的操作符，还用了一些非形式化的英语解释，给出的规范说明比较短，比较容易阅读和理解。  

③VDM 是维也纳开发方法的简称，包括一系列形式规范和开发计算机系统的技术，它源于IBM维也纳实验室的研究工作。VDM 语言有一套数学符号系统和基于谓词逻辑和集合理论的证明规则。它广泛地借用了六十年代在欧洲和美国发展的形式化语言和基于数学的技术。VDM 方法是一种基于形式语义的软件开发方法，规定了大型软件开发的三个阶段：提出要求、形式定义、开发步骤。它也是自顶向下逐步求精的开发方法。VDM 的主要特点是中间的形式定义阶段，体现了用形式语义来刻画语言的思想。VDM 方法不仅能被用于规范，而且能被用于设计和对应的实现中。它广泛应用于程序设计语言、数据库、操作系统等应用领域中。

④OBJ是一组语言的统称，基于有序类型等式逻辑(Order Sorted Equational Logic)或其它逻辑(如重写逻辑，隐含等式逻辑或一阶逻辑)，并提供了参数化模块编程能力，能够很方便地应用于形式规范和定理证明环境。最早的OBJ语言是Goguen在1976年发明的。以后逐渐演化出多个版本。如OBJ1、OBJ2等，目前最新的版本是OBJ3。此外，许多代数语言和方法也深受OBJ的影响，著名的有CafeOBJ、Maude和CoFI。

用于形式化开发的工具包括：

①现有大量的实用工具支持了B方法软件开发周期的所有阶段，包括动画和文档生成。B-Tool是一个语言翻译器也是支持B语言的运行时环境。B-Toolkit是一套集成的工具集，完全支持B方法用于形式化软件开发，B-Tllokit是基于B-Tool。这些工具可以从B-Core(UK)Limited，UK这个机构得到。基于B方法的开发工具主要有Atelier B和EdithB。Atelier B是由ClearSy开发的，是一个支持抽象机器符号的工具。特性包括：语法、类型和静态语义的检查，证据支持，求精，图形接口和打印，但是不支持测试事例的生成。B4free是一个B建模环境，是一套用于B模型开发和用户工具生成的工具集。

②Venus是一个VDM++工具集，它支持面向对象并行系统的开发，它是基于图形建模和形式化规格的。Venus有三个组件：支持OMT符号的LOV/OMT的环境；支持形式化规格语言VDM++的VPP 环境；耦合模块，由一个从类图到VDM++规格的转换器和用于定位在VDM++规格错误的图形演示工具。Venus支持一下一些活动：⑴图形化建模，包括类图的生成和处理，类图、类图转换成VDM++以及所生成的VDM++规格的一致性检查；⑵建立形式化规格；⑶原形生成；⑷文档生成。

③Cabernet工具，支持实时系统得形式化开发。它提供规范、执行和验证实时系统规格的同构框架，而这个实时系统规格是基于Petri网的时间和功能扩展。Cabernet的主要组件包括：⑴支持Petri网编辑的图形编辑器；⑵一组执行/演示/仿真套件；⑶层次型管理器；⑷工具生成器，通过集成现有的功能来动态获得复杂工具；⑸用户定制，建立新的图形符号来满足应用需求。

更多的工具包括FDR、VDM Toolbox、PVS、ELUDO LOTOS Toolset、HyTech和Amphion等。

《B方法》译者前言：裘宗燕教授  ， 北京大学数学学院信息科学系

随着计算机应用逐步渗透到社会生产生活的各个领域，我们今天看到了一种非常奇特的现象：一方面，计算机已被看做是现代科学技术开发出的最强有力的工具，是“用之万事而皆灵”的魔杖。计算机的介入改造了所有的行业和部门，不断改变着我们的工作和生活方式，是否应用了计算机已经成了评判一个行业是否现代化的最重要标志。另一方面，促成这种变化的领域本身的情况却很不令人乐观。计算机系统的不可靠也已成为人所共知的事实。在听到“是计算机系统出了问题”时，世人都已经习惯于视如天命而自认倒霉，再也没有进一步去追究责任的兴趣和意愿了。看到计算机系统正在越来越多地控制着我们周围的环境，一些系统的失误可能给人们的生命财产造成巨大损失时，作为计算机工作者难道不该不寒而栗?难道我们的软件开发工作就应该永远停留在这样的水平?系统的质量就应该永远这样没有保证吗?

实际上，人们早已开始从各种角度研究软件的开发方法和途径，研究软件开发的本质和规律性，总的目标就是希望改变目前这种基于个人技术、缺乏科学指导的软件开发方式，为将来的软件开发过程和作为其产品的软件系统提供更坚实的科学基础。软件形式化方法就是这样一个研究领域。经过几十年的努力，软件形式化方法的研究已经取得了许多重要成果，一些成果已经被应用于实际的软件开发工作，取得了很好的效果。

本书作者J-R Abrial在软件形式化方法及其应用领域中做出了非常重要的贡献。J-RAbrial从20世纪70年代开始研究数据结构和程序的形式化问题，他于20世纪70年代后期在牛津大学程序设计研究组(PRG)访问期间做了规范语言Z的开创性工作。后来Z被PRG和其他研究组织广泛研究和发展，现已成为许多计算机科学技术课程和教育项目的基础，并在英国及全欧洲的工业界得到应用，用于描述复杂软件系统的规范，支持严格化的软件系统开发过程。为使形式化方法与软件开发更平滑地衔接，J-RAbrial从20世纪80年代前期开始了B方法的研究，目的是希望为实际软件开发过程提供一个坚实的数学基础。在B方法的研究和开发中，J-RAbrial及其合作者不仅关心软件的严格规范描述问题，而且特别关注从严格规范到最终程序的演化过程(一般称为精化，refinement)，以及对这一过程的自动支持。B方法的开发从其早期开始就是与工业界的实际应用一起进步的，在其发展过程中，人们就已经用它作为工具开发了一系列关键性的应用软件系统。一个早期的重要实例是巴黎地铁列车的信号系统，这一系统为减少列车间距、提高整个地铁系统的安全性做出了显著贡献。这本《B方法》就是J-RAbrial对B方法的总结整理。

B方法是一种用于描述、设计计算机软件的严格方法，其作用一直延伸到代码生成，人们已经实现了一些工具系统，支持基于B方法的软件开发的全过程。本书完整地介绍了B方法的数学理论基础，精确定义了B方法中使用的规范语言形式，还给出了许多运用B方法进行软件开发的例子。其中一些例子有一定规模和很强的实际背景，有些例子就是实际系统的简化版本。从这本书的阅读中，我们可以看到一个复杂的软件系统可以怎样从一段有关其功能的严格描述中逐步演化出来，如何在这种演化过程中维持某些不变性，怎样保证后面做出的更加细节的描述不破坏已有的定义和已经证明的性质，如何自动地产生出这一过程中的“证明义务”。实际上，在今天的软件开发过程中，人们也在不自觉地做着这些事情，基本上是靠开发者的直觉和朴素技术去控制和解决问题。这种缺乏科学指导的不严格的方式，是软件开发过程中产生错误的一个重要原因。因此，从某种角度看，B方法(以及其他严格的软件开发方法)也就是希望把人们在软件开发中的实际工作过程整理清楚，为其建立坚实的理论基础，将其规范化和严格化。

我们常常可以听到有关“软件形式化方法有什么用”的质问，我们认为这实际上是一个错误的问题。任何不幼稚的计算机工作者都不会期望能开发出某种新技术或者新方法，一劳永逸地解决软件领域的问题。计算机软件系统是人类有史以来制造出的最复杂的产品，可具有成百万甚至成千万行代码的巨大规模，其各组成部分之间可能存在的错综复杂的直接和间接交互作用方式，其静态结构与动态行为之间构成难以琢磨的关系。我们还没有过制造和把握如此复杂的系统的需要和经验。另一方面，我们需要开发出许许多多的软件，以满足千变万化、层出不穷的实际需要，这些工作又常常必须在较低开发成本和较短开发周期的条件下完成，因此就不可能像开发基础硬件那样组织一支最优秀的庞大队伍，不可能投人足够的金钱和时间。所有这些因素造成的结果就是软件的复杂性问题将永远陪伴着我们。

由于这些情况，任何有助于我们理解、控制、管理软件系统复杂性的理论、技术或方法都是非常有价值的。今天，软件工作者们最重要的努力方向就是去克服或缓解软件复杂性的障碍。他们在许多层次上工作：通过高层管理手段组织软件开发活动；通过严格的工作规范，企图深入控制软件开发的整个过程；通过安排丰富而烦琐的人际信息交互活动，设法使在需求、设计和各个后续阶段引进的错误和不良结构可能及早被发现；通过不同抽象技术，设法隔离各个层次、各个部件内部的复杂性，提供层次间或者部件间的清晰界面；通过研究各种程序开发模型及其支持技术，使软件工作中的一些模式和难点能够被屏蔽在模型之中，得到模型的充分支持；通过各种软件的组件形式尽可能地利用已有工作成果，降低开发新软件的代价和复杂性；通过开发合适的语言和其他表述形式，以满足在各个层次上严格而方便地描述软件及其不同侧面的需要；通过各种技术手段和工具，对软件开发过程提供尽可能多的支持，或者支持人们对开发结果进行更深入的分析；通过人员的训练，提高参与软件工作的每个人的认识能力和工作能力，使他们能够成为软件质量的支点而不是潜在的破坏者；如此等等。软件形式化方法可能在许多层次上起作用。

实际上，软件形式化方法正在逐步渗入我们的日常软件开发活动。各种所谓的“无差错”或者“干净”软件开发技术，貌似新颖的“基于契约的软件开发”等，实际上不过是软件形式化方法研究成果的实践性版本。“断言”、“前条件和后条件”、“不变式”等术语已经在我们周围不绝于耳。一些国家和部门的软件开发规范已经明确提出，关键性软件的开发过程必须有软件形式化方法的参与。我们相信，终归会有一天，不知道什么是循环不变式或者数据不变式的人，将没有资格参加任何关键软件的开发工作。到了那个时候，软件的质量一定会提高到一个新水平。每个关心自己的事业和个人发展的计算机专业工作者，都必须重视这些情况。我们也希望本书的出版将能为国内计算机教育和实践提供一些参考。

作为译者，我非常感谢电子工业出版社支持出版这本形式化方法的重要著作，感谢周宏敏编辑为本书付出的辛勤劳动。最后还要感谢夏萍和丛欣对我持之以恒的支持和帮助。

Event B

       Event B是一种基于传统的谓词演算和定理证明的形式化语言。Event B 的新的特征是它引入了事件( event) 。事件( event) 是Event-B的一个重要特征，因此它非常适合用来为周期行为建模。另外，Event B支持逐步精化地建立系统模型。Event B的基本内容和要点：

（1）使用Event B建模时，首先建立一个模型（model），一个完整的 Event－B模型应该包括场景( Context) 、自动机( Machine) 、证明义务 ( Proof Obligations ) 以及精化(Refine-ment)。（2）场景中定义静态场景和常量。集合形式的常量是载体集( Sets) ，数值形式的常量是不变量( Constants) 。在场景（Context）中用公理( Axioms) 和定理( Theorems)来说明常量包括载体集和不变量，以及各个常量之间的关系和它们各自的属性。（3）自动机定义系统的动态行为。每个自动机都有状态，状态由变量的值来具体体现。不变式( Invariants)规定了变量的形式及行为，而事件执行时会改变变量的值。（4）事件就是系统中可能会发生的事情，体现了动态。而事件的执行会导致系统的状态即自动机状态的变化，具体体现就是变量的值的改变。事件一般表示为:evt·any p where G( p，v) then S( p，v，v ) end( 1)其中，p 是参数，v 是变量，G( p，v) 是事件成立的条件，S( p，v，v') 是事件的行为。（5）证明义务：需要证明改变后的变量的值仍然满足不变式的规定，即系统的状态仍然在安全的范围内，这样才能证明这些事件的执行是安全的。精化的功能是增加系统的功能、增加细节、改变状态模型。精化一个自动机过程中，可能需要增加新的变量和新的事件。一般一个模型需要进行多次精化才能符合要求。

        Event B的特色在于可以在需求设计过程中保证设计的正确性和无二义性。适合于实时性强的嵌入式控制系统的建模。目前，使用比较广泛、研究比较热门的几种需求获取方法有：  用例驱动的交互式需求获取、基于UML的需求获取、基于领域本体的需求获取、基于Event-B的软件形式化需求获取和 基于RGPS的网络式软件需求方法。基于Event-B的形式化需求获取方法，建立于离散系统模型的基础上，提出了一个可以适用于软件生命周期所有阶段的模型－公平离散系统模型，并给出了其在软件需求获取过程中求精、验证和控制复杂性的方法、需求模型复用的概念。接下来，采用Event-B完整地描述形式化的需求获取的全过程,对Event-B的模型结构进行了扩充，把从规约到程序求精和验证的概念延伸到需求获取过程中，并详细地解释了需求获取过程中需求求精验证和从规约到程序求精验证的本质区别。在需求模型复杂性控制方法上，给出了模型分解的新算法，求精过程中给出事件引入的新策略，同时详细给出了需求模型复用的策略。

在需求构建过程中，离散系统模型是对问题系统的抽象，在实现过程中，离散系统模型是对程序的抽象（它的语义等价于转移系统模型），离散系统应能很好的描述系统或程序的性质，离散系统模型应能描述系统和程序的安全性和活性。对于并发系统、反应系统和分布系统，离散系统模型还应能准确地描述系统事件被选中执行的方式，既离散系统模型应能准确的描述系统事件之间的公平性。

作为软件开发过程中使用的统一框架模型，公平离散系统模型包含如下几个组成部分：状态变量的集合、状态变量定义域和常量的集合、状态之间的转移的集合、初始化条件的集合、公平约束的集合。用符号FDSM（U，V，INIT，T,MP,WF,SF）表示：U＝{u1,u2,．．．．．un}模型内一组有穷的状态变量的集合，针对有限状态系统，所有的状态变量定义域是有限的。无穷状态系统状态变量的取值范围是无限的。V＝{v1,v2,……vn}是状态变量定义域及常量的集合，表示整个状态变量的取值范围和在这模型中所必需的常量。INIT是模型的初始条件的集合，这些条件定义出所有FDSM的初始状态，如果一个状态满足条件INIT，那么就称其为初始状态。T―模型中事件的集。MP＝{m1,m2,……,mn}是MP公平的集合,其中mi∈T,直观的解释如果m包含于MP,在一定的状态下m中的事件的卫条件为真，那么一定有部分的事件发生，且转移到下一个状态。WF＝{w1,w2,……,wn}是弱公平的集合，其中wi∈T，直观的解释如下：如果在模型的一个无穷计算序列中wi的卫条件一直为真，那么在这个计算序列中wi一定能被无限多次选中运行。SF＝{s1,s2,……,sn}是强公平的集合，其中si∈T,直观的解释如下：如果模型中的无穷计算序列中si的卫条件无穷多次为真，那么在这个计算序列中si一定能被无限多次的选中运行。

利用公平离散系统模型构建系统需求模型是一个步进的过程，在构建系统的需求时，首先开始构建一个最简单的系统模型，这个模型只具备一些大粒度的事件，验证最初的模型。验证完成之后，在个模型的基础上进一步的考察系统对获得的需求进行的扩充，在验证在扩充。这个过程和从规约到程序的过程有点类似，仿造从规约到程序演化过程的概念，把这过程也称之为求精。求精之后的需求更接近实际系统，需求求精过程和规约的演化过程有本质的区别，在规约到程序的演化过程中，涉及到数据类型和语言概念上的变化，而在需求的获取过程中数据类型是一致的，且不存在语言概念上的变化，在需求求精过程中使用的语言是完全相同。更直观的讲，需求的求精过程有点类似于观察一个事物，当距离较远时，看到的系统的特征较大，能看见的系统的行为很少，当的距离进一些时，看到的特征粒度就会小些，能看见的系统行为就比之前多些，这样逐步拉近和观察事物的距离看到的细节就越来越多，直到最终获取所观察事物的所有细节，在这个观察的过程中使用方法和借助的工具均是相同。公平离散系统模型构建系统需求方法是基于模型的方法，使用Event B作为其描述语言。公平离散系统模型由如下几部分组成：状态变量的集合、状态变量定义域和常量的集合、状态之间的转移的集合、初始化条件的集合、公平的集合。Event B的系统模型由两个主要部件组成：Model和Context。其中Model描述的是公平离散系统中状态变量、状态之间的转移、初始化条件和公平，而Context描述的模型的所需的支集和常量集合及关于支集和常量的约束，反应的是公平离散系统模型中状态变量定义域和常量。

一个基本的Event B的模型由如下四部分组成：(1)、关键字MODEL名称；(2)、状态变量的集合，对每个状态变量赋值就可以确定模型的具体的状态，在Model中用v代表；(3)、不变式约束，模型中所有状态都必需满足的一组状态谓词，由状态变量和常量组成，其值仅有真与假两种取值可能，在模型中用I(v)表示，用来限定模型的边界。(4)、事件的集合，状态间的转移，在Event－B模型中称之为事件（Event），对应于公平离散系统模型中的转移。

用Event B模型描述系统的需求模型，必需对模型中描述的软件系统的相关性质进行验证，以确保获取的系统需求模型有效性和完备性，在统一的框架下处理需求和规约，可以把在规约中用于验证完整性和有效性及一致性的规则，推广到需求模型的验证中。首先必需考虑验证模型的安全性质，其次考虑验证模型的活性性质。

近年来，J-R  abrial教授与中国学者的交流比较频繁，他曾经访问和讲学的大学包括北京大学，华东师范大学、西安电子科技大学等。

    Jean-Raymond Abrial  于2011年在西安电子科技大学软件学院讲学

参考文献：

• Review of The B-Book at the Wayback Machine (archived December 2, 2007) by Jonathan Bowen

• Managing the Construction of Large Computerized Systems — article

• Have we learned from the Wasa disaster (video) — talk by Jean-Raymond Abrial

• Abrial, Jean-Raymond (22 August 2005). "Managing the Construction of Large Computerized Systems". Department of Computer Science, ETH Zurich, Switzerland. Retrieved September 26, 2011.

• Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010年5月13日)