EVENT-B建模:系统和软件工程

Event-B是一种基于传统的谓词演算和定理证明的形式化语言,支持逐步精化地建立系统模型,适合于实时性强的嵌入式控制系统的建模，多用于工业软件系统的开发，本书为Event-B的开发者Jean-Raymond Abrial关于形式化方法的著作。 1.作者是国际有名软件和软件理论专家，首次将“B方法”系统级的工控软件高安全保障解决方案引入中国，这是目前市场上专享的一本关于Event-B的中文书籍。 2.书中包含了大量具有不同难度的练习和开发项目，方便读者对所学知识进行检验和实践。 3.书中每个例子都用Rodin平台工具集证明过，因此书本的内容十分严谨。 4.外文原版书是这一领域极具权威的教材书籍，由剑桥大学出版社出版，内容方面有很高的质量保障。

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

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

第 1章  引言 1 1.1  动机 1 1.2  各章概览 2 1.3  如何用这本书 6 1.4  形式化方法 8 1.5  一个小迂回：蓝图 9 1.6  需求文档 10 1.6.1  生命周期 10 1.6.2  需求文档的困难 10 1.6.3  一种有用的比较 11 1.7  本书中使用的“形式化方法”的定义 12 1.7.1  复杂系统 12 1.7.2  离散系统 13 1.7.3  测试推理与模型（蓝图）推理 13 1.8  有关离散模型的非形式化概览 14 1.8.1  状态和迁移 14 1.8.2  操作性解释 14 1.8.3  形式化推理 15 1.8.4  管理闭模型的复杂性 15 1.8.5  精化 15 1.8.6  分解 16 1.8.7  泛型开发 16 1.9 参考资料 17 第 2章  控制桥上的汽车 18 2.1  引言 18 2.2  需求文档 18 2.3  精化策略 20 2.4  初始模型：汽车的数量 20 2.4.1  引言 20 2.4.2  状态的形式化 21 2.4.3  事件的形式化 22 2.4.4  前-后谓词 23 2.4.5  证明不变式的保持性质 23 2.4.6  相继式 25 2.4.7  应用不变式保持性的规则 25 2.4.8  证明义务的证明 26 2.4.9  推理规则 27 2.4.10  元变量 29 2.4.11  证明 29 2.4.12  更多推理规则 30 2.4.13  改造两个事件：引进卫 31 2.4.14  改造的不变式保持规则 31 2.4.15  重新证明不变式的保持性 32 2.4.16  初始化 33 2.4.17  初始化事件init的不变式建立规则 33 2.4.18  应用不变式建立规则 34 2.4.19  证明初始化的证明义务：更多推理规则 34 2.4.20  无死锁 35 2.4.21  无死锁规则 35 2.4.22  应用无死锁证明义务规则 35 2.4.23  更多推理规则 36 2.4.24  证明无死锁的证明义务 37 2.4.25  对初始模型的总结 38 2.5  第 一次精化：引入单行桥 38 2.5.1  引言 38 2.5.2  状态的精化 39 2.5.3  精化抽象事件 40 2.5.4  重温前-后谓词 40 2.5.5  精化的非形式化证明 41 2.5.6  证明抽象事件的正确精化 42 2.5.7  应用精化规则 43 2.5.8  精化初始化事件init 45 2.5.9  初始化事件init精化正确性的证明义务规则 46 2.5.10  应用初始化精化的证明义务规则 46 2.5.11  引入新事件 46 2.5.12  空动作skip 47 2.5.13  证明两个新事件的正确性 47 2.5.14  证明新事件的收敛性 49 2.5.15  应用非收敛证明义务规则 50 2.5.16  相对无死锁 51 2.5.17  应用相对无死锁证明义务规则 51 2.5.18  更多推理规则 52 2.5.19  第 一个精化的总结 54 2.6  第二次精化：引入交通灯 55 2.6.1  精化状态 55 2.6.2  精化抽象事件 56 2.6.3  引进新事件 56 2.6.4  叠加：调整精化规则 57 2.6.5  证明事件的正确性 58 2.6.6  更多逻辑推理规则 58 2.6.7  试探性的证明和解 58 2.6.8  新事件的收敛性 64 2.6.9  相对无死锁 67 2.6.10  第二个精化的总结 68 2.7  第三次精化：引入车辆传感器 70 2.7.1  引言 70 2.7.2  精化状态 72 2.7.3  精化控制器里的抽象事件 75 2.7.4  在环境里增加新事件 77 2.7.5  新事件的收敛性 78 2.7.6  无死锁 78 第3章  冲压机控制器 79 3.1  非形式描述 79 3.1.1  基本设备 79 3.1.2  基本命令和按钮 80 3.1.3  基本用户动作 80 3.1.4  用户工作期 80 3.1.5  危险：控制器的必要性 80 3.1.6  安全门 81 3.2  设计模式 81 3.2.1  动作和反应 82 3.2.2  第 一种情况：一个简单的动作反应模式，无反作用 83 3.2.3  第二种情况：一个简单的动作模式，一次重复动作和反应 86 3.3  冲压机的需求 90 3.4  精化策略 91 3.5  初始模型：连接控制器和电动机 92 3.5.1  引言 92 3.5.2  建模 92 3.5.3  事件的总结 94 3.6  第 一次精化：把电动机按钮连接到控制器 94 3.6.1  引言 94 3.6.2  建模 95 3.6.3  加入“假”事件 99 3.6.4  事件的总结 100 3.7  第二次精化：连接控制器到离合器 100 3.8  另一个设计模式：两个强反应的弱同步 101 3.8.1  引言 101 3.8.2  建模 103 3.9  第三次精化：约束离合器和电动机 108 3.10  第四次精化：连接控制器到安全门 110 3.10.1  拷贝 110 3.10.2  事件的总结 110 3.11  第五次精化：约束离合器和安全门 110 3.12  另一设计模式：两个强反应的强同步 111 3.12.1  引言 111 3.12.2  建模 112 3.13  第六次精化：离合器和安全门之间的更多约束 117 3.14  第七次精化：把控制器连接到离合器按钮 118 3.14.1  拷贝 118 3.14.2  事件的总结 118 第4章  简单文件传输协议 120 4.1  需求 120 4.2  精化策略 120 4.3  协议的初始模型 121 4.3.1  状态 122 4.3.2  一些数学表示法 122 4.3.3  事件 125 4.3.4  证明 125 4.4  协议的第 一次精化 127 4.4.1  非形式化的说明 127 4.4.2  状态 128 4.4.3  更多数学符号 128 4.4.4  事件 130 4.4.5  精化证明 131 4.4.6  事件receive的收敛性证明 134 4.4.7  相对无死锁证明 135 4.5  协议的第二次精化 135 4.5.1  状态和事件 135 4.5.2  证明 137 4.6  协议的第三次精化 137 4.6.1  状态 137 4.6.2  事件 138 4.6.3  全称量化谓词的推理规则 138 4.7  对开发的回顾 139 4.7.1  动机和预期事件的引入 139 4.7.2  初始模型 140 4.7.3  第 一次精化 140 4.7.4  第二次精化 141 4.7.5  第三次精化 141 4.8  参考资料 142 第5章  Event-B建模语言和证明义务规则 143 5.1  Event-B表示法 143 5.1.1  引言：机器和上下文 143 5.1.2  机器和上下文的关系 143 5.1.3  上下文的结构 144 5.1.4  上下文的例子 145 5.1.5  机器的结构 145 5.1.6  机器的例子 146 5.1.7  事件 147 5.1.8  动作 147 5.1.9  事件的例子 149 5.2  证明义务规则 150 5.2.1  引言 150 5.2.2  不变式保持证明义务规则：INV 151 5.2.3  可行性证明义务规则：FIS 153 5.2.4  卫加强证明义务规则：GRD 153 5.2.5  卫归并证明义务规则：MRG 154 5.2.6  模拟证明义务规则：SIM 155 5.2.7  数值变动式证明义务规则：NAT 158 5.2.8  有穷集变动式证明义务规则：FIN 158 5.2.9  变动量证明义务规则：VAR 159 5.2.10  非确定性见证证明义务规则：WFIS 161 5.2.11  定理证明义务规则：THM 162 5.2.12  良好定义证明义务规则：WD 162 第6章  有界重传协议 163 6.1  有界重传协议的非形式说明 163 6.1.1  正常行为 163 6.1.2  不可靠的通信 163 6.1.3  协议流产 164 6.1.4  交替位 164 6.1.5  协议的最后情况 164 6.1.6  BRP的伪代码描述 165 6.1.7  有关伪代码的说明 167 6.2  需求文档 167 6.3  精化策略 168 6.4  初始模型 169 6.4.1  状态 169 6.4.2  事件 169 6.5  第 一次和第二次精化 170 6.5.1  状态 170 6.5.2  第 一次精化的事件 170 6.5.3  第二次精化的事件 171 6.6  第三次精化 171 6.6.1  状态 172 6.6.2  事件 172 6.6.3  事件之间的同步 173 6.7  第四次精化 173 6.7.1  状态 173 6.7.2  事件 174 6.7.3  事件的同步 175 6.8  第五次精化 176 6.8.1  状态 176 6.8.2  事件 177 6.8.3  事件的同步 180 6.9  第六次精化 181 6.10  参考资料 181 第7章  一个并发程序的开发1 182 7.1  分布式和并发程序的比较 182 7.1.1  分布式程序 182 7.1.2  并发程序 182 7.2  提出的实例 183 7.2.1  非形式的说明 183 7.2.2  非并发的场景展示 185 7.2.3  定义原子性 186 7.3  交错 187 7.3.1  问题 187 7.3.2  计算不同交错的数目 188 7.3.3  结果 189 7.4  并发程序的规范描述 190 7.4.1  写和读的轨迹 190 7.4.2  轨迹之间的关系 190 7.4.3  不变式的总结 193 7.4.4  事件 193 7.5  精化策略 194 7.5.1  最终精化的梗概 194 7.5.2  精化的目标 196 7.6  第 一次精化 196 7.6.1  读者状态 196 7.6.2  读事件 197 7.6.3  写者状态 198 7.6.4  写事件 198 7.7  第二次精化 200 7.7.1  状态 200 7.7.2  事件和新增的不变式 200 7.8  第三次精化 203 7.8.1  状态 203 7.8.2  事件 203 7.9  第四次精化 204 7.9.1  状态 204 7.9.2  事件 205 7.10  参考资料 206 第8章  电路的开发 207 8.1  引言 207 8.1.1  同步电路 207 8.1.2  电路与其环境的耦合 208 8.1.3  耦合的动态观点 208 8.1.4  耦合的静态观点 209 8.1.5  协调性条件 209 8.1.6  一个警告 210 8.1.7  电路的最终构造 210 8.1.8  一个非常小的示例 213 8.2  第 一个例子 214 8.2.1  非形式的规范描述 214 8.2.2  初始模型 215 8.2.3  精化电路以减少其非确定性 218 8.2.4  通过改变数据空间来精化电路 220 8.2.5  构造最后的电路 222 8.3  第二个例子：仲裁器 225 8.3.1  非形式的规范描述 225 8.3.2  初始模型 226 8.3.3  第 一次精化：让电路生成二进制输出 229 8.3.4  第二次精化 231 8.3.5  第三次精化：消除电路的非确定性 233 8.3.6  第四次精化：构造最后的电路 234 8.4  第三个例子：一种特殊的道路交通灯 234 8.4.1  非形式的规范描述 235 8.4.2  关注点分离的方法 235 8.4.3  优先权电路：初始模型 236 8.4.4  最后的Priority电路 238 8.5  Light电路 240 8.5.1  一个抽象：Upper电路 241 8.5.2  精化：加入Lower电路 242 8.6  参考资料 245 第9章  数学语言 246 9.1  相继式演算 246 9.1.1  定义 246 9.1.2  一个数学语言的相继式 248 9.1.3  初始理论 248 9.2  命题语言 249 9.2.1  语法 249 9.2.2  初始理论的扩充 250 9.2.3  派生规则 250 9.2.4  方法论 252 9.2.5  命题语言的扩充 252 9.3  谓词语言 253 9.3.1  语法 253 9.3.2  谓词和表达式 254 9.3.3  全称量词的推理规则 254 9.4  相等谓词 256 9.5  集合论语言 257 9.5.1  语法 258 9.5.2  集合论公理 258 9.5.3  基本集合运算符 259 9.5.4  基本集合运算符的推广 260 9.5.5  二元关系运算符 261 9.5.6  函数运算符 264 9.5.7  各种箭头的总结 265 9.5.8  lambda抽象和函数调用 265 9.6  布尔和算术语言 266 9.6.1  语法 266 9.6.2  皮阿诺公理和递归定义 267 9.6.3  算术语言的扩充 267 9.7  高级数据结构 269 9.7.1  反自反的传递闭包 269 9.7.2  强连通图 270 9.7.3  无穷表 271 9.7.4  有穷表 274 9.7.5  环 276 9.7.6  无穷树 277 9.7.7  有穷深度树 280 9.7.8  自由树 281 9.7.9  良定义条件和有向无环图 283 第 10章  环形网络上选领导 284 10.1  需求文档 284 10.2  初始模型 286 10.3  讨论 286 10.3.1  第 一个尝试 286 10.3.2  第二个尝试 287 10.3.3  第三个尝试 287 10.3.4  解的非形式化展示 287 10.4  第 一次精化 288 10.4.1  状态：环的形式化 288 10.4.2  状态：变量 289 10.4.3  事件 289 10.5  证明 289 10.5.1  事件elect的证明 290 10.5.2  事件accept的证明 291 10.5.3  事件reject的证明 293 10.5.4  新事件不发散的证明 293 10.5.5  无死锁的证明 293 10.6  参考资料 294 第 11章  树形网络上的同步 295 11.1  引言 295 11.2  初始模型 296 11.2.1  状态 296 11.2.2  事件 297 11.2.3  证明 297 11.3  第 一次精化 298 11.3.1  状态 298 11.3.2  事件 300 11.3.3  证明 300 11.4  第二次精化 301 11.5  第三次精化 303 11.5.1  事件ascending的精化 303 11.5.2  事件descending的精化 304 11.5.3  证明定理thm3_4 306 11.5.4  证明不变式inv3_3的保持性 306 11.6  第四次精化 308 11.7  参考资料 310 第 12章  移动代理的路由算法 311 12.1  问题的非形式化描述 311 12.1.1  抽象的非形式化描述 311 12.1.2  第 一个非形式化的精化 312 12.1.3  第二个非形式化的精化 312 12.1.4  第三个非形式化的精化：解 314 12.2  初始模型 315 12.2.1  状态 315 12.2.2  事件 316 12.2.3  证明 317 12.3  第 一次精化 318 12.3.1  状态 318 12.3.2  事件 319 12.3.3  证明 320 12.4  第二次精化 320 12.4.1  状态 320 12.4.2  事件 322 12.4.3  证明 323 12.5  第三次精化：数据精化 324 12.5.1  状态 324 12.5.2  事件 324 12.5.3  证明 325 12.6  第四次精化 325 12.7  参考资料 325 第 13章  在连通图网络上选领导 326 13.1  初始模型 326 13.1.1  状态 326 13.1.2  事件 327 13.2  第 一次精化 327 13.2.1  定义自由树 327 13.2.2  扩充状态 327 13.2.3  事件的第 一次精化 328 13.2.4  第 一次精化的证明 329 13.3  第二次精化 329 13.3.1  第二次精化的状态 329 13.3.2  事件 329 13.3.3  证明 330 13.4  第三次精化：竞争问题 330 13.4.1  引言 330 13.4.2  处理竞争的状态 331 13.4.3  处理竞争的事件 332 13.5  第四次精化：简化 332 13.6  第五次精化：引入基数 333 第 14章  证明义务的数学模型 335 14.1  引言 335 14.2  不变式保持性的证明义务规则 335 14.3  观察离散迁移系统的演化：迹 337 14.3.1  第 一个例子 338 14.3.2  迹 338 14.3.3  迹的特征 339 14.3.4  演化图 339 14.3.5  数学表示 339 14.4  用迹表示简单精化 340 14.4.1  第二个例子 340 14.4.2  比较这两个例子 341 14.4.3  简单精化：非形式化的方法 342 14.4.4  简单精化：形式化定义 342 14.4.5  考虑个别的事件 343 14.4.6  外部变量和内部变量 344 14.4.7  外部集合 345 14.5  广义精化的集合论表示 345 14.5.1  引言 346 14.5.2  精化的形式化定义 347 14.5.3  精化的充分条件：前向模拟 347 14.5.4  精化的另一充分条件：反向模拟 352 14.5.5  迹的精化 352 14.6  打破抽象和具体事件之间的一对一关系 353 14.6.1  分裂抽象事件 353 14.6.2  合并几个抽象事件 353 14.6.3  引进新事件 354 第 15章  顺序程序的开发 357 15.1  开发顺序程序的一种系统化方法 357 15.1.1  顺序程序的组成部分 357 15.1.2  把顺序程序分解为独立的事件 358 15.1.3  方法梗概 359 15.1.4  顺序程序的规范：前条件和后条件 359 15.2  一个非常简单的例子 360 15.2.1  规范 360 15.2.2  精化 361 15.2.3  推广 362 15.3  合并规则 362 15.4  例：排序数组里的二分检索 363 15.4.1  初始模型 363 15.4.2  第 一次精化 364 15.4.3  第二次精化 365 15.4.4  合并 366 15.5  例：自然数数组中的最小值 366 15.5.1  初始模型 366 15.5.2  第 一次精化 367 15.6  例：数组划分 367 15.6.1  初始模型 367 15.6.2  第 一次精化 368 15.6.3  合并 370 15.7  例：简单排序 370 15.7.1  初始模型 370 15.7.2  第 一次精化 371 15.7.3  第二次精化 371 15.7.4  合并 373 15.8  例：数组反转 373 15.8.1  初始模型 373 15.8.2  第 一次精化 374 15.9  例：链接表反转 375 15.9.1  初始模型 375 15.9.2  第 一次精化 376 15.9.3  第二次精化 377 15.9.4  第三次精化 378 15.9.5  合并 378 15.10  例：计算平方根的简单数值程序 378 15.10.1  初始模型 379 15.10.2  第 一次精化 379 15.10.3  第二次精化 379 15.11  例：内射数值函数的逆 380 15.11.1  初始模型 380 15.11.2  第 一次精化 381 15.11.3  第二次精化 382 15.11.4  实例化 383 15.11.5  第 一次实例化 383 15.11.6  第二次实例化 384 第 16章  位置访问控制器 385 16.1  需求文档 385 16.2  讨论 387 16.2.1  控制的共享 387 16.2.2  闭模型的构造 387 16.2.3  设备的行为 388 16.2.4  处理安全问题 388 16.2.5  同步问题 388 16.2.6  边界的功能 388 16.3  系统的初始模型 389 16.4  第 一次精化 390 16.4.1  状态和事件 390 16.4.2  无死锁 391 16.4.3  第 一个解 392 16.4.4  第二个解 393 16.4.5  无死锁的修正 393 16.5  第二次精化 394 16.5.1  状态和事件 394 16.5.2  同步 396 16.5.3  证明 396 16.5.4  读卡器持续阻塞的危险 396 16.5.5  避免持续阻塞的提议 396 16.5.6  最后的决定 397 16.6  第三次精化 397 16.6.1  引进读卡器 397 16.6.2  与通信网络有关的假设 398 16.6.3  变量和不变式 398 16.6.4  事件 399 16.6.5  同步 400 16.6.6  证明 400 16.7  第四次精化 400 16.7.1  与物理门有关的决策 400 16.7.2  变量和不变式：绿色链 401 16.7.3  变量和不变式：红色链 401 16.7.4  事件 402 16.7.5  同步 404 第 17章  列车系统 406 17.1  非形式的引言 406 17.1.1  非形式描述的方法论约定 407 17.1.2  行车调度员控制下的轨道网络 407 17.1.3  网络的特殊组件：道岔和交叉点 407 17.1.4  阻塞的概念 409 17.1.5  通路的概念 409 17.1.6  信号的概念 411 17.1.7  通路和阻塞保持 412 17.1.8  安全性条件 414 17.1.9  运行条件 415 17.1.10  列车的假设 415 17.1.11  事故 416 17.1.12  实例 417 17.2  精化策略 420 17.3  初始模型 420 17.3.1  状态 420 17.3.2  事件 425 17.4  第 一次精化 427 17.4.1  状态 427 17.4.2  事件 429 17.5  第二次精化 431 17.5.1  状态 432 17.5.2  事件 432 17.6  第三次精化 433 17.6.1  状态 433 17.6.2  事件 433 17.7  第四次精化 434 17.8  总结 436 17.9  参考资料 437 第 18章  一些问题 438 18.1  练习 438 18.1.1  银行 438 18.1.2  生日记录册 438 18.1.3  有一行为0的数值矩阵 439 18.1.4  有序矩阵检索 439 18.1.5  名人问题 439 18.1.6  在两个有交集的有穷数值集合里找公共元素 440 18.1.7  简单的访问控制系统 441 18.1.8  简单的图书馆 441 18.1.9  简单的电路 441 18.1.10  闹钟 442 18.1.11  连续信号的分析 442 18.2  项目 443 18.2.1  旅馆的电子钥匙系统 443 18.2.2  Earley分析器 444 18.2.3  Schorr-Wait算法 446 18.2.4  线性表封装 447 18.2.5  队列的并发访问 447 18.2.6  几乎线性的排序 448 18.2.7  终止性检查 449 18.2.8  分布式互斥 449 18.2.9  电梯 452 18.2.10  业务交易协议 453 18.3  数学的开发 454 18.3.1  良构集合和关系 454 18.3.2  不动点 456 18.3.3  递归 457 18.3.4  传递闭包 457 18.3.5  过滤器和超过滤器 458 18.3.6  拓扑 458 18.3.7  Cantor-Bernstein定理 460 18.3.8  Zermelo定理 460 18.4  参考资料 462