Event-B建模系统和软件工程
①全新正版，现货速发，7天无理由退换货②天津、成都、无锡、广东等多仓就近发货，订单最迟48小时内发出③无法指定快递④可开电子发票，不清楚的请咨询客服。
￥ 93.33 7.2折 ￥ 129 全新
仅1件
浙江嘉兴
认证卖家担保交易快速发货售后保障
作者[法] 简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial）|译者:裘宗燕
出版社人民邮电
ISBN9787115508997
出版时间2019-09
装帧其他
开本其他
定价129元
货号30717148
上书时间2024-10-12
- 在售商品 暂无
- 平均发货时间 17小时
- 好评率 暂无
商品详情
- 品相描述：全新
- 商品描述
-
导语摘要
Event-B是一种基于传统的谓词演算和定理证明的形式化语言,支持逐步精化地建立系统模型,适合于实时性强的嵌入式控制系统的建模，多用于工业软件系统的开发，本书为Event-B的开发者Jean-RaymondAbrial关于形式化方法的著作。
1.作者是国际著名软件和软件理论专家，首次将“B方法”系统级的工控软件高安全保障解决方案引入中国，这是目前市场上唯一的一本关于Event-B的中文书籍。
2.书中包含了大量具有不同难度的练习和开发项目，方便读者对所学知识进行检验和实践。
3.书中每个例子都用Rodin平台工具集证明过，因此书本的内容十分严谨。
4.外文原版书是这一领域极具权威的教材书籍，由剑桥大学出版社出版，内容方面有很高的质量保障。
目录
第 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 精化初始化事件init45
2.5.9 初始化事件init精化正确性的证明义务规则46
2.5.10 应用初始化精化的证明义务规则46
2.5.11 引入新事件46
2.5.12 空动作skip47
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 不变式保持证明义务规则：INV151
5.2.3 可行性证明义务规则：FIS153
5.2.4 卫加强证明义务规则：GRD153
5.2.5 卫归并证明义务规则：MRG154
5.2.6 模拟证明义务规则：SIM155
5.2.7 数值变动式证明义务规则：NAT158
5.2.8 有穷集变动式证明义务规则：FIN158
5.2.9 变动量证明义务规则：VAR159
5.2.10 非确定性见证证明义务规则：WFIS161
5.2.11 定理证明义务规则：THM162
5.2.12 良好定义证明义务规则：WD162
第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章 一个并发程序的开发1182
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_4306
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 第
— 没有更多了 —
以下为对购买帮助不大的评价