琼·雷蒙德·阿布里亚尔　著

在Event-B中进行形式开发的一个基本概念就是模型的概念。一个模型包含了一个离散转换的完整数学开发。它由两种类型的构件，即机器和语境组成。机器包含了一个模型的动态部分，即变量、不变量、定理、异体和事件。而语境则包含一个模型的静态部分，即载体集合、常量、公理和定理。这些分别属于机器或语境的项目称为建模元素。一个模型可以只包括语境，或只包括机器，或同时包括这两者。机器和语境之间可以有各种关系。

本书作者的意图是提供有关建模及形式推理的深刻见解，这些顿悟应该是在着手有效编码之前就具备的，因此才能正确地构建所涉及的系统。通过阅读本书，读者将学会如何对程序进行建模，更广义地说，对离散系统进行建模。而所有这一切都是通过对大脑的训练来完成的。为此读者应该学习大量的源自各种各样计算机系统开发的实例，其中包括顺序程序、并发程序及电子线路等。

读者将会了解一个程序的模型与程序本身存在相当大的区别，并且意识到有关抽象和精化这两个非常重要的概念，它们的核心思想是：一个可执行程序只能在其程序设计的最终阶段才能获得，而程序设计过程有时是漫长的，是一个对未来程序循序渐进地构建越来越准确模型的过程，该过程，与由建筑师所画的各种蓝图到建筑物最终落成的过程非常相似。作者带来了利用B形式方法，即Event—B拓展建模及设计系统的一种方法。包括了大量的练习题及练习项目，书中涉及的每一个实例都利用了Rodin平台工具箱加以证明，读者可以从网站www.event-b.org上下载该平台，免费使用。它是专门用于Event-B及其相关的插件程序的。

本书内容分成18章。1、绪论，介绍了形式方法的概念，并且明确了建模的含义；2、控制在桥上的汽车；3、机械压力控制器；4、简单文件传送协议；5、Event—B建模表示法与证明义务规则；6、有界再传输协议；7、并发程序的开发；8、电子线路的开发；9、数学语言；10、环状网络的LeaderElection协议；11、树状网络的同步；12、移动主体路由选择算法；13、连接图网络的Leader Election协议；14、用于证明义务的数学模型；15、顺序程序的开发；16、定位存取控制器；17、训练系统；18、问题，该章汇总了书中各章的所有的练习题和练习项目。

本书作者是瑞士苏黎世联邦理工学院计算机科学系的客座教授和研究员，为了撰写本书，他花费了10年以上的时间。这本实用教科书适用于有关形式方法入门或高级课程。

胡光华，退休高工

(原中国科学院物理学研究所)