Event-B建模 系统和软件工程
| 作者 |
| 埃蒙德·阿布瑞尔（Jean-Raymond Abrial） |
| 丛书名 |
| 出版社 |
| 人民邮电出版社 |
| ISBN |
| 9787115508997 |
| 简要 |
| 简介 |
| 内容简介书籍计算机书籍 这本实用的教科书适用于形式化方法的入门课程或高级课程。本书以B形式化方法的一个扩展Event-B作为工具，展示了一种完成系统建模和设计的数学方法。 简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial）是国际著名计算机科学家，曾任苏黎世联邦理工学院客座教授，他基于精化的思想提出了一种系统化的方法，教读者如何逐步构造出所期望的模型，并通过严格的证明完成对所构造模型做系统化的推理。本书将介绍如何根据实际需要去构造各种程序，以及如何更为普遍地构造各种离散系统的模型。本书提供了大量的示例，这些示例源自计算机系统开发的各个领域，包括顺序程序、并发程序和电子线路等。 本书还包含了大量具有不同难度的练习和开发项目。书中的每个例子都用Rodin平台工具集证明过。 本书适合作为高等院校计算机、软件工程、网络工程、信息安全等专业高年级本科生、研究生的教材，也可供相关领域的研究人员和技术人员参考。 |
| 目录 |
| 第 1章 引言\t1 1.1 动机\t1 1.2 各章概览\t2 1.3 如何用这本书\t6 1.4 形式化方法\t8 1.5 一个小迂回：蓝图\t9 1.6 需求文档\t10 1.6.1 生命周期\t10 1.6.2 需求文档的困难\t10 1.6.3 一种有用的比较\t11 1.7 本书中使用的“形式化方法”的定义\t12 1.7.1 复杂系统\t12 1.7.2 离散系统\t13 1.7.3 测试推理与模型（蓝图）推理\t13 1.8 有关离散模型的非形式化概览\t14 1.8.1 状态和迁移\t14 1.8.2 操作性解释\t14 1.8.3 形式化推理\t15 1.8.4 管理闭模型的复杂性\t15 1.8.5 精化\t15 1.8.6 分解\t16 1.8.7 泛型开发\t16 1.9 参考资料\t17 第 2章 控制桥上的汽车\t18 2.1 引言\t18 2.2 需求文档\t18 2.3 精化策略\t20 2.4 初始模型：限制汽车的数量\t20 2.4.1 引言\t20 2.4.2 状态的形式化\t21 2.4.3 事件的形式化\t22 2.4.4 前-后谓词\t23 2.4.5 证明不变式的保持性质\t23 2.4.6 相继式\t25 2.4.7 应用不变式保持性的规则\t25 2.4.8 证明义务的证明\t26 2.4.9 推理规则\t27 2.4.10 元变量\t29 2.4.11 证明\t29 2.4.12 更多推理规则\t30 2.4.13 改造两个事件：引进卫\t31 2.4.14 改造的不变式保持规则\t31 2.4.15 重新证明不变式的保持性\t32 2.4.16 初始化\t33 2.4.17 初始化事件init的不变式建立规则\t33 2.4.18 应用不变式建立规则\t34 2.4.19 证明初始化的证明义务：更多推理规则\t34 2.4.20 无死锁\t35 2.4.21 无死锁规则\t35 2.4.22 应用无死锁证明义务规则\t35 2.4.23 更多推理规则\t36 2.4.24 证明无死锁的证明义务\t37 2.4.25 对初始模型的总结\t38 2.5 第 一次精化：引入单行桥\t38 2.5.1 引言\t38 2.5.2 状态的精化\t39 2.5.3 精化抽象事件\t40 2.5.4 重温前-后谓词\t40 2.5.5 精化的非形式化证明\t41 2.5.6 证明抽象事件的正确精化\t42 2.5.7 应用精化规则\t43 2.5.8 精化初始化事件init\t45 2.5.9 初始化事件init精化正确性的证明义务规则\t46 2.5.10 应用初始化精化的证明义务规则\t46 2.5.11 引入新事件\t46 2.5.12 空动作skip\t47 2.5.13 证明两个新事件的正确性\t47 2.5.14 证明新事件的收敛性\t49 2.5.15 应用非收敛证明义务规则\t50 2.5.16 相对无死锁\t51 2.5.17 应用相对无死锁证明义务规则\t51 2.5.18 更多推理规则\t52 2.5.19 第 一个精化的总结\t54 2.6 第二次精化：引入交通灯\t55 2.6.1 精化状态\t55 2.6.2 精化抽象事件\t56 2.6.3 引进新事件\t56 2.6.4 叠加：调整精化规则\t57 2.6.5 证明事件的正确性\t58 2.6.6 更多逻辑推理规则\t58 2.6.7 试探性的证明和解\t58 2.6.8 新事件的收敛性\t64 2.6.9 相对无死锁\t67 2.6.10 第二个精化的总结\t68 2.7 第三次精化：引入车辆传感器\t70 2.7.1 引言\t70 2.7.2 精化状态\t72 2.7.3 精化控制器里的抽象事件\t75 2.7.4 在环境里增加新事件\t77 2.7.5 新事件的收敛性\t78 2.7.6 无死锁\t78 第3章 冲压机控制器\t79 3.1 非形式描述\t79 3.1.1 基本设备\t79 3.1.2 基本命令和按钮\t80 3.1.3 基本用户动作\t80 3.1.4 用户工作期\t80 3.1.5 危险：控制器的必要性\t80 3.1.6 安全门\t81 3.2 设计模式\t81 3.2.1 动作和反应\t82 3.2.2 第 一种情况：一个简单的动作反应模式，无反作用\t83 3.2.3 第二种情况：一个简单的动作模式，一次重复动作和反应\t86 3.3 冲压机的需求\t90 3.4 精化策略\t91 3.5 初始模型：连接控制器和电动机\t92 3.5.1 引言\t92 3.5.2 建模\t92 3.5.3 事件的总结\t94 3.6 第 一次精化：把电动机按钮连接到控制器\t94 3.6.1 引言\t94 3.6.2 建模\t95 3.6.3 加入“假”事件\t99 3.6.4 事件的总结\t100 3.7 第二次精化：连接控制器到离合器\t100 3.8 另一个设计模式：两个强反应的弱同步\t101 3.8.1 引言\t101 3.8.2 建模\t103 3.9 第三次精化：约束离合器和电动机\t108 3.10 第四次精化：连接控制器到安全门\t110 3.10.1 拷贝\t110 3.10.2 事件的总结\t110 3.11 第五次精化：约束离合器和安全门\t110 3.12 另一设计模式：两个强反应的强同步\t111 3.12.1 引言\t111 3.12.2 建模\t112 3.13 第六次精化：离合器和安全门之间的更多约束\t117 3.14 第七次精化：把控制器连接到离合器按钮\t118 3.14.1 拷贝\t118 3.14.2 事件的总结\t118 第4章 简单文件传输协议\t120 4.1 需求\t120 4.2 精化策略\t120 4.3 协议的初始模型\t121 4.3.1 状态\t122 4.3.2 一些数学表示法\t122 4.3.3 事件\t125 4.3.4 证明\t125 4.4 协议的第 一次精化\t127 4.4.1 非形式化的说明\t127 4.4.2 状态\t128 4.4.3 更多数学符号\t128 4.4.4 事件\t130 4.4.5 精化证明\t131 4.4.6 事件receive的收敛性证明\t134 4.4.7 相对无死锁证明\t135 4.5 协议的第二次精化\t135 4.5.1 状态和事件\t135 4.5.2 证明\t137 4.6 协议的第三次精化\t137 4.6.1 状态\t137 4.6.2 事件\t138 4.6.3 全称量化谓词的推理规则\t138 4.7 对开发的回顾\t139 4.7.1 动机和预期事件的引入\t139 4.7.2 初始模型\t140 4.7.3 第 一次精化\t140 4.7.4 第二次精化\t141 4.7.5 第三次精化\t141 4.8 参考资料\t142 第5章 Event-B建模语言和证明义务规则\t143 5.1 Event-B表示法\t143 5.1.1 引言：机器和上下文\t143 5.1.2 机器和上下文的关系\t143 5.1.3 上下文的结构\t144 5.1.4 上下文的例子\t145 5.1.5 机器的结构\t145 5.1.6 机器的例子\t146 5.1.7 事件\t147 5.1.8 动作\t147 5.1.9 事件的例子\t149 5.2 证明义务规则\t150 5.2.1 引言\t150 5.2.2 不变式保持证明义务规则：INV\t151 5.2.3 可行性证明义务规则：FIS\t153 5.2.4 卫加强证明义务规则：GRD\t153 5.2.5 卫归并证明义务规则：MRG\t154 5.2.6 模拟证明义务规则：SIM\t155 5.2.7 数值变动式证明义务规则：NAT\t158 5.2.8 有穷集变动式证明义务规则：FIN\t158 5.2.9 变动量证明义务规则：VAR\t159 5.2.10 非确定性见证证明义务规则：WFIS\t161 5.2.11 定理证明义务规则：THM\t162 5.2.12 良好定义证明义务规则：WD\t162 第6章 有界重传协议\t163 6.1 有界重传协议的非形式说明\t163 6.1.1 正常行为\t163 6.1.2 不可靠的通信\t163 6.1.3 协议流产\t164 6.1.4 交替位\t164 6.1.5 协议的最后情况\t164 6.1.6 BRP的伪代码描述\t165 6.1.7 有关伪代码的说明\t167 6.2 需求文档\t167 6.3 精化策略\t168 6.4 初始模型\t169 6.4.1 状态\t169 6.4.2 事件\t169 6.5 第 一次和第二次精化\t170 6.5.1 状态\t170 6.5.2 第 一次精化的事件\t170 6.5.3 第二次精化的事件\t171 6.6 第三次精化\t171 6.6.1 状态\t172 6.6.2 事件\t172 6.6.3 事件之间的同步\t173 6.7 第四次精化\t173 6.7.1 状态\t173 6.7.2 事件\t174 6.7.3 事件的同步\t175 6.8 第五次精化\t176 6.8.1 状态\t176 6.8.2 事件\t177 6.8.3 事件的同步\t180 6.9 第六次精化\t181 6.10 参考资料\t181 第7章 一个并发程序的开发1\t182 7.1 分布式和并发程序的比较\t182 7.1.1 分布式程序\t182 7.1.2 并发程序\t182 7.2 提出的实例\t183 7.2.1 非形式的说明\t183 7.2.2 非并发的场景展示\t185 7.2.3 定义原子性\t186 7.3 交错\t187 7.3.1 问题\t187 7.3.2 计算不同交错的数目\t188 7.3.3 结果\t189 7.4 并发程序的规范描述\t190 7.4.1 写和读的轨迹\t190 7.4.2 轨迹之间的关系\t190 7.4.3 不变式的总结\t193 7.4.4 事件\t193 7.5 精化策略\t194 7.5.1 最终精化的梗概\t194 7.5.2 精化的目标\t196 7.6 第 一次精化\t196 7.6.1 读者状态\t196 7.6.2 读事件\t197 7.6.3 写者状态\t198 7.6.4 写事件\t198 7.7 第二次精化\t200 7.7.1 状态\t200 7.7.2 事件和新增的不变式\t200 7.8 第三次精化\t203 7.8.1 状态\t203 7.8.2 事件\t203 7.9 第四次精化\t204 7.9.1 状态\t204 7.9.2 事件\t205 7.10 参考资料\t206 第8章 电路的开发\t207 8.1 引言\t207 8.1.1 同步电路\t207 8.1.2 电路与其环境的耦合\t208 8.1.3 耦合的动态观点\t208 8.1.4 耦合的静态观点\t209 8.1.5 协调性条件\t209 8.1.6 一个警告\t210 8.1.7 电路的最终构造\t210 8.1.8 一个非常小的示例\t213 8.2 第 一个例子\t214 8.2.1 非形式的规范描述\t214 8.2.2 初始模型\t215 8.2.3 精化电路以减少其非确定性\t218 8.2.4 通过改变数据空间来精化电路\t220 8.2.5 构造最后的电路\t222 8.3 第二个例子：仲裁器\t225 8.3.1 非形式的规范描述\t225 8.3.2 初始模型\t226 8.3.3 第 一次精化：让电路生成二进制输出\t229 8.3.4 第二次精化\t231 8.3.5 第三次精化：消除电路的非确定性\t233 8.3.6 第四次精化：构造最后的电路\t234 8.4 第三个例子：一种特殊的道路交通灯\t234 8.4.1 非形式的规范描述\t235 8.4.2 关注点分离的方法\t235 8.4.3 优先权电路：初始模型\t236 8.4.4 最后的Priority电路\t238 8.5 Light电路\t240 8.5.1 一个抽象：Upper电路\t241 8.5.2 精化：加入Lower电路\t242 8.6 参考资料\t245 第9章 数学语言\t246 9.1 相继式演算\t246 9.1.1 定义\t246 9.1.2 一个数学语言的相继式\t248 9.1.3 初始理论\t248 9.2 命题语言\t249 9.2.1 语法\t249 9.2.2 初始理论的扩充\t250 9.2.3 派生规则\t250 9.2.4 方法论\t252 9.2.5 命题语言的扩充\t252 9.3 谓词语言\t253 9.3.1 语法\t253 9.3.2 谓词和表达式\t254 9.3.3 全称量词的推理规则\t254 9.4 相等谓词\t256 9.5 集合论语言\t257 9.5.1 语法\t258 9.5.2 集合论公理\t258 9.5.3 基本集合运算符\t259 9.5.4 基本集合运算符的推广\t260 9.5.5 二元关系运算符\t261 9.5.6 函数运算符\t264 9.5.7 各种箭头的总结\t265 9.5.8 lambda抽象和函数调用\t265 9.6 布尔和算术语言\t266 9.6.1 语法\t266 9.6.2 皮阿诺公理和递归定义\t267 9.6.3 算术语言的扩充\t267 9.7 高级数据结构\t269 9.7.1 反自反的传递闭包\t269 9.7.2 强连通图\t270 9.7.3 无穷表\t271 9.7.4 有穷表\t274 9.7.5 环\t276 9.7.6 无穷树\t277 9.7.7 有穷深度树\t280 9.7.8 自由树\t281 9.7.9 良定义条件和有向无环图\t283 第 10章 环形网络上选领导\t284 10.1 需求文档\t284 10.2 初始模型\t286 10.3 讨论\t286 10.3.1 第 一个尝试\t286 10.3.2 第二个尝试\t287 10.3.3 第三个尝试\t287 10.3.4 解的非形式化展示\t287 10.4 第 一次精化\t288 10.4.1 状态：环的形式化\t288 10.4.2 状态：变量\t289 10.4.3 事件\t289 10.5 证明\t289 10.5.1 事件elect的证明\t290 10.5.2 事件accept的证明\t291 10.5.3 事件reject的证明\t293 10.5.4 新事件不发散的证明\t293 10.5.5 无死锁的证明\t293 10.6 参考资料\t294 第 11章 树形网络上的同步\t295 11.1 引言\t295 11.2 初始模型\t296 11.2.1 状态\t296 11.2.2 事件\t297 11.2.3 证明\t297 11.3 第 一次精化\t298 11.3.1 状态\t298 11.3.2 事件\t300 11.3.3 证明\t300 11.4 第二次精化\t301 11.5 第三次精化\t303 11.5.1 事件ascending的精化\t303 11.5.2 事件descending的精化\t304 11.5.3 证明定理thm3_4\t306 11.5.4 证明不变式inv3_3的保持性\t306 11.6 第四次精化\t308 11.7 参考资料\t310 第 12章 移动代理的路由算法\t311 12.1 问题的非形式化描述\t311 12.1.1 抽象的非形式化描述\t311 12.1.2 第 一个非形式化的精化\t312 12.1.3 第二个非形式化的精化\t312 12.1.4 第三个非形式化的精化：解\t314 12.2 初始模型\t315 12.2.1 状态\t315 12.2.2 事件\t316 12.2.3 证明\t317 12.3 第 一次精化\t318 12.3.1 状态\t318 12.3.2 事件\t319 12.3.3 证明\t320 12.4 第二次精化\t320 12.4.1 状态\t320 12.4.2 事件\t322 12.4.3 证明\t323 12.5 第三次精化：数据精化\t324 12.5.1 状态\t324 12.5.2 事件\t324 12.5.3 证明\t325 12.6 第四次精化\t325 12.7 参考资料\t325 第 13章 在连通图网络上选领导\t326 13.1 初始模型\t326 13.1.1 状态\t326 13.1.2 事件\t327 13.2 第 一次精化\t327 13.2.1 定义自由树\t327 13.2.2 扩充状态\t327 13.2.3 事件的第 一次精化\t328 13.2.4 第 一次精化的证明\t329 13.3 第二次精化\t329 13.3.1 第二次精化的状态\t329 13.3.2 事件\t329 13.3.3 证明\t330 13.4 第三次精化：竞争问题\t330 13.4.1 引言\t330 13.4.2 处理竞争的状态\t331 13.4.3 处理竞争的事件\t332 13.5 第四次精化：简化\t332 13.6 第五次精化：引入基数\t333 第 14章 证明义务的数学模型\t335 14.1 引言\t335 14.2 不变式保持性的证明义务规则\t335 14.3 观察离散迁移系统的演化：迹\t337 14.3.1 第 一个例子\t338 14.3.2 迹\t338 14.3.3 迹的特征\t339 14.3.4 演化图\t339 14.3.5 数学表示\t339 14.4 用迹表示简单精化\t340 14.4.1 第二个例子\t340 14.4.2 比较这两个例子\t341 14.4.3 简单精化：非形式化的方法\t342 14.4.4 简单精化：形式化定义\t342 14.4.5 考虑个别的事件\t343 14.4.6 外部变量和内部变量\t344 14.4.7 外部集合\t345 14.5 广义精化的集合论表示\t345 14.5.1 引言\t346 14.5.2 精化的形式化定义\t347 14.5.3 精化的充分条件：前向模拟\t347 14.5.4 精化的另一充分条件：反向模拟\t352 14.5.5 迹的精化\t352 14.6 打破抽象和具体事件之间的一对一关系\t353 14.6.1 分裂抽象事件\t353 14.6.2 合并几个抽象事件\t353 14.6.3 引进新事件\t354 第 15章 顺序程序的开发\t357 15.1 开发顺序程序的一种系统化方法\t357 15.1.1 顺序程序的组成部分\t357 15.1.2 把顺序程序分解为独立的事件\t358 15.1.3 方法梗概\t359 15.1.4 顺序程序的规范：前条件和后条件\t359 15.2 一个非常简单的例子\t360 15.2.1 规范\t360 15.2.2 精化\t361 15.2.3 推广\t362 15.3 合并规则\t362 15.4 例：排序数组里的二分检索\t363 15.4.1 初始模型\t363 15.4.2 第 一次精化\t364 15.4.3 第二次精化\t365 15.4.4 合并\t366 15.5 例：自然数数组中的最小值\t366 15.5.1 初始模型\t366 15.5.2 第 一次精化\t367 15.6 例：数组划分\t367 15.6.1 初始模型\t367 15.6.2 第 一次精化\t368 15.6.3 合并\t370 15.7 例：简单排序\t370 15.7.1 初始模型\t370 15.7.2 第 一次精化\t371 15.7.3 第二次精化\t371 15.7.4 合并\t373 15.8 例：数组反转\t373 15.8.1 初始模型\t373 15.8.2 第 一次精化\t374 15.9 例：链接表反转\t375 15.9.1 初始模型\t375 15.9.2 第 一次精化\t376 15.9.3 第二次精化\t377 15.9.4 第三次精化\t378 15.9.5 合并\t378 15.10 例：计算平方根的简单数值程序\t378 15.10.1 初始模型\t379 15.10.2 第 一次精化\t379 15.10.3 第二次精化\t379 15.11 例：内射数值函数的逆\t380 15.11.1 初始模型\t380 15.11.2 第 一次精化\t381 15.11.3 第二次精化\t382 15.11.4 实例化\t383 15.11.5 第 一次实例化\t383 15.11.6 第二次实例化\t384 第 16章 位置访问控制器\t385 16.1 需求文档\t385 16.2 讨论\t387 16.2.1 控制的共享\t387 16.2.2 闭模型的构造\t387 16.2.3 设备的行为\t388 16.2.4 处理安全问题\t388 16.2.5 同步问题\t388 16.2.6 边界的功能\t388 16.3 系统的初始模型\t389 16.4 第 一次精化\t390 16.4.1 状态和事件\t390 16.4.2 无死锁\t391 16.4.3 第 一个解\t392 16.4.4 第二个解\t393 16.4.5 无死锁的修正\t393 16.5 第二次精化\t394 16.5.1 状态和事件\t394 16.5.2 同步\t396 16.5.3 证明\t396 16.5.4 读卡器持续阻塞的危险\t396 16.5.5 避免持续阻塞的提议\t396 16.5.6 最后的决定\t397 16.6 第三次精化\t397 16.6.1 引进读卡器\t397 16.6.2 与通信网络有关的假设\t398 16.6.3 变量和不变式\t398 16.6.4 事件\t399 16.6.5 同步\t400 16.6.6 证明\t400 16.7 第四次精化\t400 16.7.1 与物理门有关的决策\t400 16.7.2 变量和不变式：绿色链\t401 16.7.3 变量和不变式：红色链\t401 16.7.4 事件\t402 16.7.5 同步\t404 第 17章 列车系统\t406 17.1 非形式的引言\t406 17.1.1 非形式描述的方法论约定\t407 17.1.2 行车调度员控制下的轨道网络\t407 17.1.3 网络的特殊组件：道岔和交叉点\t407 17.1.4 阻塞的概念\t409 17.1.5 通路的概念\t409 17.1.6 信号的概念\t411 17.1.7 通路和阻塞保持\t412 17.1.8 安全性条件\t414 17.1.9 运行条件\t415 17.1.10 列车的假设\t415 17.1.11 事故\t416 17.1.12 实例\t417 17.2 精化策略\t420 17.3 初始模型\t420 17.3.1 状态\t420 17.3.2 事件\t425 17.4 第 一次精化\t427 17.4.1 状态\t427 17.4.2 事件\t429 17.5 第二次精化\t431 17.5.1 状态\t432 17.5.2 事件\t432 17.6 第三次精化\t433 17.6.1 状态\t433 17.6.2 事件\t433 17.7 第四次精化\t434 17.8 总结\t436 17.9 参考资料\t437 第 18章 一些问题\t438 18.1 练习\t438 18.1.1 银行\t438 18.1.2 生日记录册\t438 18.1.3 有一行为0的数值矩阵\t439 18.1.4 有序矩阵检索\t439 18.1.5 名人问题\t439 18.1.6 在两个有交集的有穷数值集合里找公共元素\t440 18.1.7 简单的访问控制系统\t441 18.1.8 简单的图书馆\t441 18.1.9 简单的电路\t441 18.1.10 闹钟\t442 18.1.11 连续信号的分析\t442 18.2 项目\t443 18.2.1 旅馆的电子钥匙系统\t443 18.2.2 Earley分析器\t444 18.2.3 Schorr-Wait算法\t446 18.2.4 线性表封装\t447 18.2.5 队列的并发访问\t447 18.2.6 几乎线性的排序\t448 18.2.7 终止性检查\t449 18.2.8 分布式互斥\t449 18.2.9 电梯\t452 18.2.10 业务交易协议\t453 18.3 数学的开发\t454 18.3.1 良构集合和关系\t454 18.3.2 不动点\t456 18.3.3 递归\t457 18.3.4 传递闭包\t457 18.3.5 过滤器和超过滤器\t458 18.3.6 拓扑\t458 18.3.7 Cantor-Bernstein定理\t460 18.3.8 Zermelo定理\t460 18.4 参考资料\t462 |
有问题微信扫码联系