Event-B建模系统和软件工程

图书标准信息

• 作者 [法]简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial） 著；裘宗燕 译
• 出版社 人民邮电出版社
• 出版时间 2019-09
• 版次 1
• ISBN 9787115508997
• 定价 129.00元
• 装帧 平装
• 开本 16开
• 纸张 胶版纸
• 页数 462页
• 字数 722千字

【内容简介】

这本实用的教科书适用于形式化方法的入门课程或高级课程。本书以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