简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial） 法国计算机科学家，国际知名的形式化方法和软件工程专家，欧洲科学院院士。20世纪80年代，他先后开发了著名的Z语言和B方法。2000年以后，他开发了Event-B方法，并领导一个国际团队，在欧盟项目支持下，为Event-B开发了公开免费的Rodin平台。这些语言和方法被国际形式化方法领域广泛接受和使用，并被开发工作者应用于软件和其他系统的实际开发工作。阿布瑞尔教授长期致力于推动和参与形式化方法的工业应用，指导了B方法在轨道交通领域的*早开发工作，在相关领域做出了卓越的贡献。阿布瑞尔教授与国内一些高校和研究单位有长期而密切的合作关系，并于2016年获得了中华人民共和国国务院颁发的“中华人民 共和国国际科学技术合作奖”。

第1章 引言
1.1 动机
1.2 各章概览
1.3 如何用这本书
1.4 形式化方法
1.5 一个小迂回：蓝图
1.6 需求文档
1.6.1 生命周期
1.6.2 需求文档的困难
1.6.3 一种有用的比较
1.7 本书中使用的“形式化方法”的定义
1.7.1 复杂系统
1.7.2 离散系统
1.7.3 测试推理与模型（蓝图）推理
1.8 有关离散模型的非形式化概览
1.8.1 状态和迁移
1.8.2 操作性解释
1.8.3 形式化推理
1.8.4 管理闭模型的复杂性
1.8.5 精化
1.8.6 分解
1.8.7 泛型开发
1.9 参考资料
第 2章 控制桥上的汽车
2.1 引言
2.2 需求文档
2.3 精化策略
2.4 初始模型：限制汽车的数量
2.4.1 引言
2.4.2 状态的形式化
2.4.3 事件的形式化
2.4.4 前-后谓词
2.4.5 证明不变式的保持性质
2.4.6 相继式
2.4.7 应用不变式保持性的规则
2.4.8 证明义务的证明
2.4.9 推理规则
2.4.10 元变量
2.4.11 证明
2.4.12 更多推理规则
2.4.13 改造两个事件：引进卫
2.4.14 改造的不变式保持规则
2.4.15 重新证明不变式的保持性
2.4.16 初始化
2.4.17 初始化事件init的不变式建立规则
2.4.18 应用不变式建立规则
2.4.19 证明初始化的证明义务：更多推理规则
2.4.20 无死锁
2.4.21 无死锁规则
2.4.22 应用无死锁证明义务规则
2.4.23 更多推理规则
2.4.24 证明无死锁的证明义务
2.4.25 对初始模型的总结
2.5 第 一次精化：引入单行桥
2.5.1 引言
2.5.2 状态的精化
2.5.3 精化抽象事件
2.5.4 重温前-后谓词
2.5.5 精化的非形式化证明
……
第3章 冲压机控制器
第4章 简单文件传输协议
第5章 Event-B建模语言和证明义务规则
第6章 有界重传协议
第7章 一个并发程序的开发
第8章 电路的开发
第9章 数学语言
第10章 环形网络上选领导
第11章 树形网络上的同步
第12章 移动代理的路由算法
第13章 在连通图网络上选领导
第14章 证明义务的数学模型
第15章 顺序程序的开发
第16章 位置访问控制器
第17章 列车系统
第18章 一些问题

这本实用的教科书适用于形式化方法的入门课程或高级课程。本书以B形式化方法的一个扩展Event-B作为工具，展示了一种完成系统建模和设计的数学方法。
简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial）是国际著名计算机科学家，曾任苏黎世联邦理工学院客座教授，他基于精化的思想提出了一种系统化的方法，教读者如何逐步构造出所期望的模型，并通过严格的证明完成对所构造模型做系统化的推理。本书将介绍如何根据实际需要去构造各种程序，以及如何更为普遍地构造各种离散系统的模型。本书提供了大量的示例，这些示例源自计算机系统开发的各个领域，包括顺序程序、并发程序和电子线路等。
本书还包含了大量具有不同难度的练习和开发项目。书中的每个例子都用Rodin平台工具集证明过。
本书适合作为高等院校计算机、软件工程、网络工程、信息安全等专业高年级本科生、研究生的教材，也可供相关领域的研究人员和技术人员参考。