网路协定的形式化分析与设计 _生活百科

文章插图
网路协定的形式化分析与设计【网路协定的形式化分析与设计】《网路协定的形式化分析与设计》是2003年6月电子工业出版社出版的图书，作者是古天龙。本书主要介绍了网路协定分析与设计中的形式化方法与技术。
基本介绍书名：网路协定的形式化分析与设计
作者：古天龙
ISBN：7505386468
页数：367
出版社：电子工业出版社
出版时间：2003 年6月
开本：16开
基本信息出版日期：2003 年6月开本：16开页码：367版次：1-1内容简介计算机网路及数据通信是当今信息社会的基石，网路协定则是其中不可缺少的重要组成部分。形式化方法与技术已经渗透到网路协定开发的整个过程。本书主要内容包括：网路协定及开发概论；网路协定的形式化模型；网路协定的形式描述语言；网路协定的形式化验证；网路协定的形式化综合；网路协定的测试；网路协定的分析验证工具；电子商务协定的形式化分析等。本书可作为计算机、通信、自动化等专业高年级本科生或研究生的教学用书，也可供相关领域的研究和工程技术人员参考。图书目录第1章网路协定及开发概论1.1 早期的通信及协定1.1.1 早期的通信系统1.1.2 协定缺陷的教训1.2 通信与计算机的结合1.2.1 数据通信1.2.2 计算机网路1.3 网路协定及其基本元素1.3.1 网路协定的定义1.3.2 网路协定的基本要素1.3.3 简单协定的分析1.4 分层结构与osi模型1.4.1 分层结构的意义1.4.2 osi模型1.5 网路协定的开发过程思考与练习第2章协定的形式化模型2.1 有限状态机（fsm）2.1.1 fsm的基本定义2.1.2 fsm的化简与複合.2.1.3 协定的fsm模型2.2 petri网2.2.1 petri网的基本定义2.2.2 petri网的性质2.2.3 petri网的分析2.2.4 协定的petri网模型2.3 时态逻辑(tl)2.3.1 基本术语2.3.2 时态逻辑系统2.3.3 协定的tl模型2.4 通信进程演算2.4.1 ccs的基本定义2.4.2 ccs的扩展2.4.3 协定的ccs模型思考与练习第3章网路协定的形式描述语言3.1 estelle3.1.1 概述3.1.2 模组及相关概念3.1.3 模组通信3.1.4 状态转换3.1.5 estelle描述举例3.2 lotos3.2.1 概述3.2.2 进程及相关概念3.2.3 行为运算元3.2.4 抽象数据类型3.2.5 lotos描述举例3.3 sdl3.3.1 概述3.3.2 结构的定义3.3.3 进程的行为3.3.4 通信机制3.3.5 数据3.3.6 sdl描述举例思考与练习第4章协定的形式化验证4.1 协定性质概述4.2 系统断言语言4.2.1 字元串及其运算4.2.2 抽象结构4.2.3 断言语言ctl4.2.4 ctl运算元的不动点特性4.2.5 ctl描述举例4.3 不变性分析4.4 可达性分析4.5 符号模型检验4.5.1 有序二叉判决图4.5.2 基于obdd的符号模型检验思考与练习第5章协定的形式化综合5.1 概述5.2 fsm网及其性质5.3 协定的串列综合5.4 协定的交替功能综合5.5 冲突和同步的解决方法5.5.1 竞争冲突解决策略5.5.2 冲突标识方法5.5.3 同步的充要条件思考与练习第6章网路协定的测试6.1 协定测试概述6.1.1 一致性测试6.1.2 故障模型6.1.3 协定测试结构6.1.4 协定测试级别6.1.5 协定测试流程6.2 协定测试语言ttcn6.2.1 ttcn简介6.2.2 ttcn－3核心语言6.2.3 简单测试案例6.3 控制流测试序列设计6.3.1 测试的基本假设6.3.2 测试序列生成算法6.4 数据流测试序列设计6.4.1 数据流测试的概念6.4.2 数据流测试序列生成思考与练习第7章协定的分析验证工具7.1 spin工具7.1.1 概述7.1.2 promela语言7.1.3 spin的套用7.2 smv工具7.2.1 概述7.2.2 smv输入语言7.2.3 smv的套用思考与练习第8章电子商务协定的形式化分析8.1 电子商务协定设计概述8.2 典型电子商务协定8.2.1 set协定8.2.2 netbill协定8.2.3 digicash协定8.3 电子商务协定的逻辑分析8.3.1 逻辑分析概述8.3.2 ban逻辑8.3.3 kailar逻辑8.4 电子商务协定的模型检验分析8.4.1 模型检验分析概述8.4.2 安全性的模型检验分析8.4.3 原子性的模型检验分析思考与练习参考文献