![网络协议的形式化分析与设计](https://cover.qianqiantushu.cc/40/s68e5032.jpg)
![网络协议的形式化分析与设计](https://cover.qianqiantushu.cc/40/s68e5032.jpg)
网络协议的形式化分析与设计PDF电子书下载
- 电子书积分:13 积分如何计算积分?
- 作 者:古天龙,蔡国永著
- 出 版 社:北京:电子工业出版社
- 出版年份:2003
- ISBN:7505386468
- 页数:367 页
第1章 网络协议及开发概论 1
1.1 早期的通信及协议 1
1.1.1 早期的通信系统 1
1.1.2 协议缺陷的教训 6
1.2 通信与计算机的结合 8
1.2.1 数据通信 9
1.2.2 计算机网络 10
1.3 网络协议及其基本元素 15
1.3.1 网络协议的定义 15
1.3.2 网络协议的基本要素 16
1.3.3 简单协议的分析 19
1.4 分层结构与OSI模型 21
1.4.1 分层结构的意义 22
1.4.2 OSI模型 25
1.5 网络协议的开发过程 30
思考与练习 35
第2章 协议的形式化模型 37
2.1 有限状态机(FSM) 37
2.1.1 FSM的基本定义 37
2.1.2 FSM的化简与复合 42
2.1.3 协议的FSM模型 45
2.2 Petri网 54
2.2.1 Petri网的基本定义 54
2.2.2 Petri网的性质 58
2.2.3 Petri网的分析 62
2.2.4 协议的Petri网模型 68
2.3 时态逻辑(TL) 71
2.3.1 基本术语 71
2.3.2 时态逻辑系统 73
2.3.3 协议的TL模型 76
2.4.1 CCS的基本定义 79
2.4 通信进程演算 79
2.4.2 CCS的扩展 82
2.4.3 协议的CCS模型 85
思考与练习 89
第3章 网络协议的形式描述语言 91
3.1 ESTELLE 91
3.1.1 概述 91
3.1.2 模块及相关概念 93
3.1.3 模块通信 98
3.1.4 状态转换 104
3.1.5 ESTELLE描述举例 106
3.2 LOTOS 121
3.2.1 概述 121
3.2.2 进程及相关概念 123
3.2.3 行为算子 127
3.2.4 抽象数据类型 130
3.2.5 LOTOS描述举例 137
3.3 SDL 147
3.3.1 概述 147
3.3.2 结构的定义 149
3.3.3 进程的行为 152
3.3.4 通信机制 152
3.3.5 数据 155
3.3.6 SDL描述举例 156
思考与练习 161
第4章 协议的形式化验证 163
4.1 协议性质概述 163
4.2 系统断言语言 165
4.2.1 字符串及其运算 166
4.2.2 抽象结构 168
4.2.3 断言语言CTL 170
4.2.4 CTL算子的不动点特性 173
4.2.5 CTL描述举例 175
4.3 不变性分析 176
4.4 可达性分析 180
4.5 符号模型检验 186
4.5.1 有序二叉判决图 186
4.5.2 基于OBDD的符号模型检验 196
思考与练习 200
第5章 协议的形式化综合 202
5.1 概述 202
5.2 FSM网及其性质 203
5.3 协议的串行综合 205
5.4 协议的交替功能综合 207
5.5.1 竞争冲突解决策略 210
5.5 冲突和同步的解决方法 210
5.5.2 冲突标识方法 218
5.5.3 同步的充要条件 220
思考与练习 221
第6章 网络协议的测试 223
6.1 协议测试概述 223
6.1.1 一致性测试 223
6.1.2 故障模型 224
6.1.3 协议测试结构 226
6.1.4 协议测试级别 229
6.1.5 协议测试流程 231
6.2 协议测试语言TTCN 232
6.2.1 TTCN简介 232
6.2.2 TTCN-3核心语言 236
6.2.3 简单测试案例 255
6.3.1 测试的基本假设 260
6.3 控制流测试序列设计 260
6.3.2 测试序列生成算法 261
6.4 数据流测试序列设计 272
6.4.1 数据流测试的概念 272
6.4.2 数据流测试序列生成 273
思考与练习 276
第7章 协议的分析验证工具 277
7.1 SPIN工具 277
7.1.1 概述 277
7.1.2 Promela语言 279
7.1.3 SPIN的应用 290
7.2 SMV工具 302
7.2.1 概述 302
7.2.2 SMV输入语言 303
7.2.3 SMV的应用 312
思考与练习 319
第8章 电子商务协议的形式化分析 321
8.1 电子商务协议设计概述 321
8.2 典型电子商务协议 324
8.2.1 SET协议 324
8.2.2 Netbill协议 334
8.2.3 Digicash协议 335
8.3 电子商务协议的逻辑分析 336
8.3.1 逻辑分析概述 336
8.3.2 BAN逻辑 337
8.3.3 Kailar逻辑 340
8.4 电子商务协议的模型检验分析 346
8.4.1 模型检验分析概述 346
8.4.2 安全性的模型检验分析 347
8.4.3 原子性的模型检验分析 354
思考与练习 360
参考文献 362
- 《水面舰艇编队作战运筹分析》谭安胜著 2009
- 《计算机网络与通信基础》谢雨飞,田启川编著 2019
- 《中国铁路人 第三届现实主义网络文学征文大赛一等奖》恒传录著 2019
- 《分析化学》陈怀侠主编 2019
- 《指向核心素养 北京十一学校名师教学设计 英语 七年级 上 配人教版》周志英总主编 2019
- 《设计十六日 国内外美术院校报考攻略》沈海泯著 2018
- 《影响葡萄和葡萄酒中酚类特征的因素分析》朱磊 2019
- 《计算机辅助平面设计》吴轶博主编 2019
- 《高校转型发展系列教材 素描基础与设计》施猛责任编辑;(中国)魏伏一,徐红 2019
- 《仪器分析技术 第2版》曹国庆 2018
- 《医学源流论》(清)徐灵胎著;古求知校注 2019
- 《人工智能实战》(古)阿纳达·佩雷兹·卡斯塔诺(AmaldoPerezCastano)著 2019
- 《核心心理学 申荷永斐恩讲座》申荷永著 2020
- 《锂硫电池原理及正极的设计与构建》张义永著 2020
- 《初中生物小组合作学习探索与实践》古中标 2019
- 《话说赵宋王朝》吴传永著 2018
- 《冒险去,鲁滨孙! 拯救冰棍共和国 1》(韩)姜溶范,(韩)宣喜永著;(韩)李宇逸绘;邓楠译 2013
- 《小仓山房尺牍 言文对照 新式标点 2》袁枚原著;媚古居士鉴定 1931
- 《建设社会主义新农村 河北省香河县安平镇发展方式的转变》钱津,刘增禄,许胜永著 2013
- 《冒险去,鲁滨孙! 拯救冰棍共和国 2》(韩)姜溶范,(韩)宣喜永著 2013
- 《电子测量与仪器》人力资源和社会保障部教材办公室组织编写 2009
- 《少儿电子琴入门教程 双色图解版》灌木文化 2019
- 《指向核心素养 北京十一学校名师教学设计 英语 七年级 上 配人教版》周志英总主编 2019
- 《北京生态环境保护》《北京环境保护丛书》编委会编著 2018
- 《指向核心素养 北京十一学校名师教学设计 英语 九年级 上 配人教版》周志英总主编 2019
- 《通信电子电路原理及仿真设计》叶建芳 2019
- 《高等院校旅游专业系列教材 旅游企业岗位培训系列教材 新编北京导游英语》杨昆,鄢莉,谭明华 2019
- 《电子应用技术项目教程 第3版》王彰云 2019
- 《中国十大出版家》王震,贺越明著 1991
- 《近代民营出版机构的英语函授教育 以“商务、中华、开明”函授学校为个案 1915年-1946年版》丁伟 2017