网络编程协议

网络协议分析

2018-06-25  本文已影响0人  丿曰

第一章 概述

一、协议定义

  1. 为网络中互相通信的对等实体间进行数据交换二建立的规则、标准或约定,保证实体在计算机网络中有序地交换数据。


    实体及对等实体.png
  2. 协议是关于分布式系统进行信息交换时地一种约定,协议应按照语言地方式进行定义。即:网络协议就是具有规定文法、语法和语义地语言。


    文法语法及语义
  3. 延伸为计算机通信协议
    协议时计算机网络和分布式系统中各种通信实体或进程间相互交换信息是必须遵守的一组规则或约定。

二、协议三要素

语法、语义、同步

  1. 语法
    网络协议中地语法体现为数据报文中的控制信息和各种控制报文的结构、格式
  2. 语义
    协议数据报文中的控制信息和控制报文所约定的含义,即需要完成何种动作发出何种控制信息做出何种响应
  3. 同步
    同步是指事件发生顺序的详细说明。具体来说,同步是指通信过程中各种控制报文传送的顺序关系
    常用建立通信双方的有限状态机的方法来描述网络协议。

三、网络体系结构

采用层次式结构

网络体系结构=计算机网络的各层+各层协议的集合

ISO的OSI/RM:

七层模型

IETF的TCP/IP:
网络访问层、互联网层、传输层、应用层

TCP/IP协议结构

四、协议标准化

符合其用途
促进贸易、交流和技术转让
简化以提高可用性
规定一类设备必须能够执行的任务或者描述一个装置和它的安全特征。

五、协议工程

协议工程

1. 协议工程学用形式化方法描述协议设计和维护中的各个过程。

2. 协议工程过程

集成化、形式化的协议开发过程。

目的:减少协议开发过程中潜在的错误,提高协议开发的效率,促进协议标准化的发展。

3. 协议开发过程

协议设计、形式描述、验证、实现、测试、运行

协议开发过程

设计

根据协议的需求说明构造协议的非形式描述文本称为协议设计。
包括:协议环境分析、协议的功能设计、协议组织形式的确定、协议元素的构造、协议文本的编制等。
遵循原则:结构化、模块化等。
结果:非形式描述协议文本。

形式描述

形式描述模型
1. 有限状态机FSM
2. Petri网
形式描述语言
CCITT制定的SDL

验证

两项工作

1.在语法和语义方面进行验证
2.进行计算机模拟

验证的主要内容

1.可达性分析
2.死锁和活锁检测
3.协议的有界性和完整性检查
4.协议的动作序列检查
5.通道溢出检查等

验证方法

1.模型检查
最常见方法:可达性分析。包括状态穷举、状态随机枚举、状态概率枚举等方法
2.证明:推理演算,严密证明
3.模拟:通过模拟试验测试协议的各种性质

实现

协议实现是指由协议规范到协议的可执行目标代码的过程
协议实现的自动化:协议工程的主要目的之一。
通过形式化描述技术可实现半自动化。步骤:
1.利用翻译程序将协议的形式描述文本转换成与机器无关的源代码
2.手工编写与机器有关的、在协议规范中没有描述的问题的处理代码。

测试

验证一个协议的实现,主要考虑:
1.协议一致性测试
1.1 检测新协议实现是否能满足该协议规范所规定的规则。
1.2 如果协议实现不能通过一致性测试,则说明该协议实现与其他同样通过一致性测试的协议实现不能在同一个全局系统中很好地协调工作。
1.3 一致性测试的基础:FDT
1.4 一致性测试要解决的问题:
-> 测试系统设计
测试方法和测试系统体系结构
-> 测试序列的产生
“彻底性”、“标准化”。测试序列的自动生成和形式化描述。
1.5 测试序列生成器
可以产各种可能发生的情况组合,测试所实现的协议是否在各种正常非正常情况下均能正确工作。
2.对协议实现的评价。
要求
1.彻底性 须彻底测试所实现的协议
2.标准化 使用的测试集须是标准的

性能

主要包括吞吐量和时延
目的:
改善协议机制,提高执行效率。

协议维护

六、思考题

1.“软件工程”和“协议工程”的关系。
区别:
协议工程比软件工程更加一体化,形式化。协议工程的目的是减少协议开发过程中潜在的错误,提高协议开发效率,促进协议标准化的发展。
协议工程的开发过程包括:
设计,描述,验证,实现,性能分析和测试
软件工程的开发过程包括:
可行性分析,需求分析,概要设计,详细设计,具体开发。
联系:
协议工程和软件工程都是为了简化开发过程,协议工程时以协议软件为研究对象的软件工程。
2.选择一个网络协议,说明该协议的三要素。

第二章 协议设计

一、两种标准

1. OSI/RM

法律上的国际标准——开放系统互联参考模型,并没有得到市场的认可。只要遵循OSI标准,一个系统就可以和位于世界上任何地方的、也遵循这同一标准的其他任何系统进行通信。

1.1 各层基本功能

ISO/OSI各层基本功能

1.2 OSI失败的原因

  1. OSI的专家们缺乏实际经验,他们在完成OSI标准时缺乏商业驱动力;
  2. OSI的协议实现起来过于复杂,而且运行效率很低;
  3. OSI标准的制定周期太长,因而使得OSI标准生产的设备无法及时进入市场;
  4. OSI的层次划分不太合理,有些功能在多个层次中重复出现。

2. TCP/IP

非国际标准,但常被称为事实上的国际标准。

2.1 TCP/IP各层对应的主要协议

TCP/IP各层及主要协议

2.2 IP数据包的转发过程

整体情况
在具体的物理网络的链路层,只能看见MAC帧而看不见IP数据报。IP层抽象的互联网屏蔽了下层很复杂的细节,在抽象的网络层上讨论问题,就能够使用 统一的、抽象的IP地址,研究主机和主机或主机和路由器之间的通信
个别情况

两个路由器的IP地址并不出现在IP数据报的首部中,路由器只根据目的站的IP地址的网络号进行路由选择

路由情况

二、为什么要分层

1. 分层的好处

2. 不分层的后果

如果不分层,每一个新的应用程序都必须为每个网络重新实现一次。

三、OSI模型的核心

服务、接口、协议

服务与协议是完全分离的,服务涉及层与层之间的接口,协议涉及不同机器上两个对等实体之间发送的数据包

四、n层协议模型

协议模型

1. 实体

在OSI中,实体(entity)表示任何可以发送和接收信息的硬件或软件进程。在许多情况下,实体就是一个特定的模块。

2. SP-服务原语

在进行交互时所要交换的一些必须信息或命令,以表明需要本地的或远端的对等实体做什么事情。

3. SAP-服务访问点

同一系统相邻两层的实体进行交互的地方。服务用户通过在一个SAP递交数据并从另一个SAP读出。

4. 服务

一个(n)实体向上一层所提供的服务由以下三部分构成:
(1) (n)实体自己提供的某些功能。
(2) 通过与处在另一系统中的对等(n)实体的通信而得到的服务。
(3) 从(n-1)层及其以下各层以及本地系统环境得到的服务。

服务与协议:
本层的服务用户只能看见服务而无法看见下面的协议。下面的协议对上面的服务用户是透明的。
协议是“水平的”,即协议是控制对等实体之间通信的规则。
服务是“垂直的”,即服务是由下层向上层通过层间接口提供的。
“透明”-指存在但看不见的事物
“虚拟”-指看起来存在但实际上不存在的事物

5. 协议数据单元PDU

将(n)层对等实体之间,为实现该层协议所交换的信息单元称为协议数据单元PDU (Protocol Data Unit)。通常将第n层的协议数据单元记为(n)PDU。

6. 服务数据单元SDU

OSI将层与层之间交换的数据的单元称为服务数据单元SDU。
一个(n)服务数据单元就是(n)服务所要传送的逻辑数据单元。

PDU与SDU的区别与联系:
SDU就是数据PDU中的用户数据,但不一定是一一对应关系。
可以是多个SDU合成为一个PDU(称为“拼装”),也可以是将一个SDU划分为几个PDU(称为“分段”)。

PDU和SDU

7. 通道

N层中任何两个协议实体通过(n-1)SAP所形成的逻辑数据通路称为(n-1)层通道。

n层协议的通信环境:

1.用户应用要求
2.(n-1)层通道(Channel)的性质
3.n层协议运行时的操作系统和硬件环境

通道的类型:

1.空通道-报文的发送时间和延迟时间为0的通道
2.非缓冲通道-通道中 最多只有一个正在传送中的报文
3.缓冲通道-允许有多个报文停留的通道

通道性质:

(n-1)层通道的性质对n层协议的构成有非常重要的影响

1.通道的形成方式

A和B建立并独占一条连接,此时(n-1)层应提供有连接服务
A和B与其它协议实体一起共享一条连接
A和B利用(n-1)层提供的无连接服务进行通信
如果(n-1)层为物理层,A和B可独占一条物理信道,或共享一条物理信道

2.通道的队列性质

除物理层外,一般可将(n-1)层通道看作是队列通道。
即一个数据报文从n层源端协议实体发出之后要在n层以下各层多次存贮转发,在每个存贮转发处就存在一个队列。
队列的主要性质是平均队列长度以及最大队列允许长度
队列越长,那么数据报文在通道中的时延就会越大;
如果队列长度达到最大允许长度,那么后续的数据报文将会丢失 。

3.回程时延RTT

RTT是从n层源端实体发出报文到该报文的确认信息到达该实体之间的时间间隔,它包括目标实体收到报文之后,对报文进行处理然后发出确认信息的时间。

时延的产生
4.差错特性
5.可靠性

通道的可靠性是指通道无故障,如连接中断、复位等。

6.报文的最大长度或最大传输单元MTU

通道所能接收的最大报文长度。主要影响n层协议的报文分段、拼接等功能。

7.工作方式

-单工、半双工、全双工
-同步与异步

8.通信方式
  1. 点对点-任意两个N 层协议实体利用一条(N - 1)层通道通信,协同完成指定协议功能。如TCP连接,UDP点对点方式。
  2. 点对多点-任意两个以上N 层协议实体利用多条(N - 1)层通道通信,协同执行一定的任务。如ATM的点对多点连接,UDP的广播方式。
9.安全性

对用户数据加密和安全控制(如口令、权限)

10.通道的带宽

通信线路的带宽也称通频带,用频率来度量。
通道的带宽可进一步分为前向带宽、后向带宽、峰值带宽等。

五、协议提供的服务

1. 面向连接的服务

2. 无连接的服务

3. 思考题

  1. 面向连接的服务和无连接服务的选择。
    答:
    强调数据传输的完整性、可靠性和可控制性时,选择面向连接的服务。
    强调数据传输性能时,选择无连接的服务。
  2. HTTP协议利用有连接的TCP作为传输通道,并不断建立连接和断开连接。这样做的好处与坏处分别是什么。
    答:
    好处:管理简单,存在的连接都是有用的连接。一定程度保证完整性、可靠性。
    坏处:如果请求过于频繁,将在TCP的建立与关闭上浪费时间和带宽。

六、协议功能

(N)层协议为了向上一层提供服务,必须实现一定的功能。

1. 基本的协议功能的类型

1.1 连接管理

两种连接:

点对点、点对多点

三种主要功能:
连接建立

双方协商工作参数:初始序号
信用量、QoS。协商失败则连接建立失败。

连接释放

突然释放-立即关闭
文明释放-成功发送所有数据后关闭

连接维护

如Keep-alive查询、参数变更等。

针对延迟的保护措施:

1.2 数据交换

数据的发送与接收:
协议支持的用户数据、类型:

块数据、流数据、批数据、优先数据、带外数据、紧急数据、编码数据。

实现数据传输的子功能:

1.3 差错控制

差错:丢失、重复、乱序等。
(n-1)通道提供的数据通道的可靠性越高,则n层协议需实现的差错控制机制则越少。

序号:

序号是确认和重传的基础,此外序号可用于流量控制。

1)三种不同的产生方式
2)如何防止序号重复

使用一个非常大的序号空间。
使得在数据单元从一端到另一端的最大可能延迟时间L内,所有从源点发送出去的新数据单元都有不同的序号。

3)序号空间的大小与信道特点、确认方法、流量控制方法和PDU中的数据字段长度有关
确认:

接收者显式地通知发送者所发送的数据的接受情况

1) 被确认的对象
2)确认的情况
3)确认分为三种类型
4)两种发送方式

在一种协议中,通常两种确认形式并存。

5)如何标识被确认的对象

用被确认的数据 PDU或字节的序号来标识

6)累计确认

如果否定确认或肯定确认的语义是表示所给定的序号之前的所有序号(包括或不包括本序号)的数据PDU都已被成功地接收了,则该确认又称为累计确认。

计时器:

检测数据PDU、确认PDU或重传请求信号的丢失。

1)超时值的设置
2)计时器超时值设置不当会导致什么后果?

如果超时值设置太短,连续大量的数据重传,严重情况下将加剧网络的拥塞程度,出现更多数据丢失 ;
如果超时值设置太长,出现数据丢失而得不到及时纠正,也会降低协议的性能。

3)TCP协议中的计时器
重传:

发送者重传:

1)基于滑动窗口的重传方法

1.4 流量控制

指“接收端控制发送端的数据发送速率以消除接收端缓存溢出的可能性,并使网络不致过载”

1)为什么使用流量控制?
2)举例

1.5 拥塞控制

在某段时间,若对网络中某一资源(链路容量、交换节点中的缓冲区、处理机)的需求超过了网络所能提供的可用部分,网络的性能就要降低。这种情况就叫做拥塞(congestion)。

1)拥塞控制的主要功能
2)拥塞控制与流量控制地区别和联系

区别:
流量控制只在一对给定的发送方和接收方之间,控制发送方以不超过接收方处理能力的速率发送数据。
拥塞控制是一个全局性的过程,涉及到网络中所有的主机、所有的路由器,以及与降低网络传输性能有关的所有因素。

联系:
流量控制限制了进入网络中地信息总量,可以在一定程度上减缓拥塞地作用。

2. 其他功能

七、协议元素

协议三要素

语法、语义、同步

协议的主体

状态-事件转换机制

协议六元素

并不是所有协议都必须包含以下六种元素。多个协议功能组成一个完整的协议之后,这六种元素一般使必须的。

元素之间的有机联系:在什么协议状态下,在什么输入事件驱动下,调用什么协议过程;协议过程在什么条件下(谓词),采取什么协议动作(操作),输出什么事件或修改哪些协议状态和变量。
在上述元素中,通常用状态变迁表或状态转换图来描述协议的状态、事件、操作和谓词。

1. 服务原语及其时序

一般用服务规范(Service Specification)来定义和描述N层协议向外部所提供的服务。
服务规范定义了服务用户和服务提供者之间的交互作用的规则,包括:服务原语和服务原语时序。
N 层协议的服务原语和原语参数详细准确地描述了N层协议和它的服务用户之间的接口。

1)根据服务原语对服务的分类:

1.需要证实的服务
2.不需要证实的服务

2)一个完整的服务原语通常包括

原语名字、原语类型、原语参数


原语

2. PDU及其时序

N层协议的PDU从语法和语义上详细准确地定义了n层协议实体之间交换的信息(PDU编码格式/协议使用的词汇表)。

3. 协议状态

N层协议必须定义所有的协议状态。

4. 协议事件

1)根据用途分类
2)根据事件的作用范围分类
3)协议事件的三个性质

5. 协议变量

保存协议运行的历史数据、运行参数的变量,以及协议机制本身所设置的变量。

常见的协议变量:

6. 协议操作和谓词

每种协议功能都是通过一组协议过程的执行来实现的。
协议过程:协议在输入事件的驱动下,在一定条件下,执行一系列的操作或动作。

一定条件:
这些约束条件涉及协议参数、协议变量、协议运行环境等。将描述这些约束条件的语句称之为谓词(predicate)。

这些操作包括:
-产生输出事件
-清楚和设置计时器
-修改协议变量
-改变协议状态

原子过程:
原子过程包含多个协议操作,并且过程一旦启动之后,所有包括的操作一次性完成,不经历中间协议状态,不被其它过程打断。
一般来说,在协议运行时,可将它从一个状态到另一个状态的转换处理成原子过程。

八、协议组织

协议组织是指将相关协议功能和协议元素组成一个完整协议的过程。

这个过程涉及以下技术和方法:

1. 协议层次化

如果n层协议的功能和结构仍然很复杂,可将n层协议的众多功能进一步分成多个子层。
子层的划分可使复杂协议的结构变得清晰,有利于协议的设计、验证、实现和测试。但是,子层的划分可能降低协议性能。

2.协议阶段化

可将n层协议分成多个运行阶段,每个阶段只涉及到一部分协议功能。如OSI体系结构的运输层协议的正常运行被分为三个阶段:连接建立阶段、数据传输阶段、连接释放阶段。

3.协议分类

由于不同用户的需求以及协议的运行环境的不同导致协议的复杂性。因此,可以将协议分成不同类别或不同级别,每类协议只适用于特定用户和特定环境,那么复杂协议就会变得简单。

4.运行方式

协议运行方式有三种:

九、协议文本

协议文本是协议设计阶段的最终结果。
协议文本中,最重要、最主要部分是协议元素的描述。必须对每一项协议元素作出准确、清晰、无二义性的定义。此外,协议的各元素是有机联系的,协议文本应清晰表达这些关系。

十、协议设计方法

1. 设计原则

其中,最基本的是:简单和模块化

2. 分层的原则

3. 自顶向下的设计方法

协议设计方法

第三章 协议形式化描述技术

一、形式化技术的产生

过去人么习惯使用自然语言描述协议。
优点:方便易懂
缺点:不严格、不精确、结构不好、没有描述标准、有二义性。不同的人对协议描述的理解不同。难以进行验证、实现和测试自动化。

解决办法:形式化技术

是将协议工程各阶段在技术上衔接起来的纽带。

形式描述模型FDM

形式描述语言FDL

模型与语言

模型:
对象或系统的抽象(OSI/RM)
描述对象或系统的方法或技术(FSM/PetriNet)

形式语言:
具有严格的语法和语义;
可精确、完全表述协议的功能及行为;
以一种或多种数学方法或形式模型为基础。如SDL基于扩展的FSM和抽象数据类型。

二、FSM

1. 有限状态机FSM的几个概念

状态(State)

指的是对象在其生命周期中的一种状况,处于某个特定状态中的对象必然会满足某些条件、执行某些动作或者是等待某些事件。

事件(Event)

指的是在时间和空间上占有一定位置,并且对状态机来讲是有意义的事情。事件通常会引起状态的变迁,促使状态机从一种状态切换到另一种状态。

转换、转移、变迁、迁移(Transition)

指的是两个状态之间的一种关系,表明对象将在第一个状态中执行一定的动作,并将在某个事件发生且满足某个特定条件时进入第二个状态。

动作(Action)

指的是状态机中可以执行的原子操作,所谓原子操作指的是它们在运行的过程中不能被其他消息所中断,必须一直执行下去。

2. 形式化定义

FSM和非确定FSM,可以看成仅接收输入并发生状态改变,但无任何输出的自动机。


FSM的形式化定义

对于不确定的有限自动机NFA,其下一时刻状态为一个状态子集。

3. Moore机和Mealy机

具有输出的自动机器模型按照输出的不同分成两类:

Moore机在接收输入串的过程中不断改变状态并在每个状态上有字符输出。
Mealy机只是在接收输入串的过程中不断改变状态,并且字符输出与当前状态及输入串有关。

有限状态机可看作是Moore机的一个特例
Moore机可看作是Mealy机的一个特例

Moore机FSM形式化定义
Mealy机FSM形式化定义

4. 如何设计FSM

5. FSM的优点

6. 停等协议

停等协议甲乙双方

将甲乙两方各自的有限状态机合在一起,用一个有限状态机来描述整个系统。这回导致状态数目大大增加,因此需要合并一些状态,考虑一些次要的细节。


合并后的状态变迁图

7. FSM的简化

8. FSM的错误模型

可达性分析:
死锁
活锁
无限分支
不可达状态

其他:
输出错
转移错
输出转移错

9. EFSM

FSM的缺点:

FSM扩展模型地目的:

其中,明显的缺点为:
FSM不能方便地描述对变量地操作
缺少描述任意数值的传送能力

从两个方面对FSM进行扩展:

三、PetriNet

Petri网是一种图形化的数学工具,适合于描述和分析并发、异步、分布式的系统,特别便于描述系统中进程或组件的顺序、并发、冲突以及同步等关系。
Petri网也是一种状态变迁模型,它允许同时发生多个状态变迁,因而Petri网是一种并发模型。可用来描述通信系统中各异步组件之间的关系。

Petri网所处的状态是由标记的分布来决定的。

1. Petri网形式化定义

Petri网的四元组

2. Petri网的状态变迁

发生变迁的条件:

标记移动规则:

发生点火后,标记要重新分布。

一个简单的例子:

图1
图2
图3

状态变迁类型:

3. PetriNet的扩充

4. PetriNet的性质

行为性质:

1)可达性
2)有界性
3)活性

活性:反映的是系统中无死锁的特性。

变迁t的活性等级划分:
L0 - 没有任何一个变迁序列可以引发变迁t,即该变迁是“死的”
L1 - 在某些变迁序列中,变迁t至少被引发一次
L2 - 在某些变迁序列中,变迁t至少被引发k次
L3 - 在某些变迁序列中,变迁t可无限次被引发
L4 - 在每个变迁序列中,变迁t至少被引发一次

4)可逆性

在一个Petri网中,如果存在一个引发序列σ=t1, t2, …, tn,使得从该Petri网的任一可达标记向量M出发可以返回到初始标记向量M0,则称该Petri网是可逆的。

5)可覆盖性

在一个Petri网中,对于标记向量M,如果存在一标记向量M′,任一位置p,都有:位置p在M′中的分量的值都大于等于该位置在M中的分量的值,则称标记向量M是可覆盖的。

6)可持续性

在一个Petri网中,如果对于任何两个满足变迁条件的变迁,其中一个变迁被引发以后,另一个变迁仍然满足变迁条件,则称该Petri网是可持续的。

7)公平性

在一个Petri 网中,对于两个变迁t1, t2,如果其中一个变迁可以引发 而另一个变迁不可引发的这种情况出现的最大次数是有界的,称这两个变迁具有有界公平关系。
如果该Petri网中,任意一对变迁都存在有界公平关系,则称该Petri网为有界公平网。

结构性质:

5. Petri网在协议描述中的应用

不编号的停等协议 编号的停等协议

第四章 协议形式描述语言(SDL)

SDL是基于扩展有限状态机抽象数据类型的混合技术。SDL既可描述系统的概要设计,亦可描述系统的详细设计。

一、SDL的三种语法形式

1. 图形表示的SDL/PR

较适合于描述系统的结构和控制流

2. 用文字短语表示的SDL/PR

较适合于机器处理

3. 程序语言形式的SDL,X.250

二、SDL系统结构

1. 概述

在SDL中,整个系统由多个互连的抽象机(扩展的有限状态机FSM)所组成。
每个抽象机的动态行为由其他抽象机或环境的交互和对交互数据的操作来描述。

SDL/PR使用的主要符号:


SDL/PR使用的主要符号

2. SDL的静态结构

一个SDL应用的静态结构由系统、功能块、进程、过程和通道构成。

SDL的静态结构

1)系统

规范所描述的对象称为一个系统。
根据系统与环境之间是否有交互,将系统分为开放的和封闭的。

一个系统的规范描述由以下部分组成:
所有通道、信号(Signal)、信号表(Signal List)、预定义的数据类型与/或宏(macro)的定义;一个或多个功能块。

2)功能块

功能块含有进程,并用来构造系统。功能块通过通道互连,并通过通道连接到系统边界。
在描述功能块时,进程、过程(Procedure)、服务类型、数据类型和信号均可作为功能块描述规范的一部分。

3)进程

可保留和处理数据,数据受进程的局部变量(由该进程定义)约束。
利用信号,数据值可在进程之间传送,也可传送给环境或从环境接收。

4)通道

通道充当功能块之间以及功能块与系统边界之间传输信号的媒介。既可以是单方向的,也可以是双方向的。

在SDL中,将系统、功能块、进程等称为代理。各个代理用块图来表示,一个代理可以对应多个块图。

三、SDL对系统动态行为的描述

1. SDL的结构化概念

系统中的每一个功能块由一组进程或一组子功能块组成,进程间通过信号路由(Signal routes)或功能块的子结构(Substructure)相连接。
子功能块又可由一组进程或一组子功能块组成。这样可得到一个系统的分级多层描述:功能块树 (Tree of Blocks)

2. 动态行为描述

四、SDL中的数据

在SDL中,数据的定义一般基于抽象数据类型。
“抽象数据类型”是指其定义并不描述(数据)类型是如何实现的,而仅仅描述当将操作符(Operators)应用到该类型的数值上时产生何种结果。

1. SDL预定义数据类型

SDL定义了一些预定义的数据类型,
如布尔(Boolean)、整数(Integer)、自然数(Natural)、实数(Real)、字符(Character)、字符串(Charstring)、进程标识符(PId)、时刻(Time)、持续时间(Duration)。
此外,SDL还预定义了一些产生器(Generator),
如数组(Array)、串(String)、计时器(Timer)和幂集(Powerset)等。
这些预定义的数据类型可在任何级别上的SDL描述中使用。
用户还可用上述数据类型自行定义其他的数据类型。

2. 类

在SDL中,类(Sort) 是值的集合。集合中的元素个数可以是有限的,也可以是无限的,但不能为空。
一般来说,SDL中的数据类型定义包括三个部分:类定义,操作符(Operators)定义和等价式(Equations)定义

1)类定义

例:Boolean类定义


Boolean类定义

第五章 协议验证技术

一、验证的含义

正确性
完整性
一致性

验证协议的实现 一致性测试

Verification 在功能方面验证
Validation 语法方面验证

二、验证的方法

1. 非形式化验证

主要通过遍历和代码检查

2. 形式化验证

以形式描述技术为前提,主要将形式描述技术与推理技术结合。
一方面可以获得无二义性的协议规范,另一方面可以借助计算机辅助工具来帮助实施自动或半自动验证。

1)模型检测/模型检查/模型检验

本质上是用严密的数学方法来验证设计是否满足预设的需求,从而自动化地发现设计中的错误。是一种检查给定模型是否满足某一逻辑规则的方法。

2)演绎验证方法

定理证明方法:

三、协议性质

协议验证的最主要任务是检查协议是否满足规定的协议性质。

也有文献将其分为安全性和活动性。
活动性体现在终止性和进展性两个方面。

1. 一般性质

1)可达性

协议的各种可能状态之间的可达关系。

2. 特殊性质

3. 一般性质和特殊性质

协议验证着重于一般性质
协议测试着重于特殊性质

四、可达性分析

检查协议描述中是否有不可达,死锁、未定义、活锁等协议模型错误;包括状态穷举,状态随机枚举,状态概率枚举等方法。

可达性分析是最常用的协议验证方法,它试图产生和检查协议所有或部分可达状态。

可达性分析的三个重要技术:
怎样找出所有可达状态,构成可达图。
怎样检测死锁、活锁等协议错误。
怎样解决状态空间爆炸问题。

可达性分析练习

1. 可达性分析原理:

采用穷举法检查同一层内两个或多个协议实体间所有可能的交互所产生的全局状态。
从一个给定的初始状态开始,触发所有可能的变迁(用户命令、超时、消息发送、接收等),产生新的全局状态。
对每一个新产生的状态重复执行上述过程直到没有新的状态产生(某些变迁将导致系统返回到已产生的状态)。
对于一个给定的初始状态,这种分析能够确定协议可能产生的所有结果。

2. 可达性分析算法

1)穷尽性可达性分析算法

穷尽性可达性分析算法

先广搜索的优点:优先发现执行序列短的错误状态;
先深搜索方法的优点之一是占用存贮空间小。
假定每个状态有两个后继状态,算法执行m步之后,对于先深搜索方法,W的长度为m;而对于先广搜索方法,W的长度为2m。

2)受控部分搜索算法

一般来说,受控部分搜索算法较全局搜索方法有效和可行。但是,这种方法不能保证协议无错。通常需要执行多次才能得到比较可信的结果。

3)随机模拟算法

随机模拟/随机遍历


随机模拟算法

随机模拟算法与协议系统的大小和复杂性无关,即使是无限大的系统,也可以应用。因此,对于复杂的验证问题,这种算法也许是唯一可用的方法。

4)三种算法的比较

3. 基于可达性分析的协议错误检测

4. 状态空间爆炸问题的解决

五、不变性分析

如果一个系统的某个性质能用一个确定的逻辑表达式描述,并且恒为真(不随系统的状态变化或执行序列而改变),那么这个性质称为系统的不变性质,简称为系统不变性(system invariance)。

1. 不变性分析的途径

1)不变性证明系统

采用归纳法:
验证初始状态的不变性表达式是否成立;
假定某个状态的不变性成立,验证从该状态开始的所有相关事件过程中不变性是否成立。

2)不变性监测系统

借助监测软件和监测方法对模拟运行或符号执行中的协议进行不变性校验的过程称之为不变性监测。

第七章 一致性测试技术

验证一项新的协议实现,通常需要进行多项测试。一般要考虑以下四个方面:

一、 一致性测试与验证

“一致性测试”的目的是检查一个给定协议实现的外部行为是否符合协议的规范。
“验证”检查形式化规范的逻辑正确性。

二、 功能测试与结构测试

三、 一致性测试的前提

假定协议标准本身是正确的。

通过一致性测试可以给用户提供两个信息:
通过了一致性测试的协议实现,具有协议所要求的各种能力。
在具有代表性的通信实例中,被测试的协议实现的外部特性与协议标准的要求一致。

四、一致性测试要求

DCR和SCR
动态一致性是指协议规范中规定的通信实例中的协议实现所必须呈现的外部特性的组合或允许的各种选择性组合;
而静态一致性是指协议规范中为了使协议实现能够互连而定义的功能类别、功能单元的分组以及选择性功能等。

五、一致性测试级别

ISO 9646将协议一致性测试分为四级,由低到高分别为

行为测试可分两级:
覆盖性测试:只要求测试序列历经IUT的所有变迁至少一次即可。
穷尽性测试:要求检查每个变迁的前后状态。

六、一致性测试模型

七、一致性测试流程

八、一致性测试方法

一致性测试方法决定了 测试集的产生和描述方法测试执行系统的结构 等。
ISO 9646中定义了四种标准的抽象测试方法:

本地测试法:


本地测试法

分布式测试法:


分布式测试法

协同测试法:


协同测试法

远程测试法:


远程测试法

上述这几种测试法是最基本的,适于单层协议测试,有许多变种,如渡船测试法(Ferry Method)、多方测试法及骑跨式(Astride)测试法等。

九、测试集

测试集包括两部分:
测试序列
测试数据

对同一测试序列的事件施加不同的测试数据(即测试事件携带不同参数),就产生不同的测试例。一个测试序列对应多个测试例。

测试集具有层次结构:
  1. 测试集由多个测试组组成。每一测试组覆盖某一类测试目的。
    比较常用的测试组划分方法是根据协议的不同状态,为每一状态的测试目的集合构造一个测试组。测试组由多个测试例组成,每一测试例针对某一测试目的。
  2. 利用测试步(Test Step) ,可以将测试例模块化。所有测试步都是按照测试事件的顺序或其它较小的测试步来定义的,因此,全部测试步等效于测试事件的序列。
  3. 测试事件是测试例和测试步的最小单位,是测试步内规范的基本单元。


    测试集的层次结构

十、测试表示方法

描述测试系统和IUT的行为。

通用的协议测试表示方法需满足的要求:
  1. 所描述的测试集应该是系统独立的。
  2. 可以描述任一协议的一致性测试集。
  3. 能为测试集的设计人员提供自动或半自动支持工具以加快测试集开发过程。
  4. 降低整个测试集的开发和维护费用。
  5. 提高协议一致性测试集的标准化程度,以增强开放系统之间的互操作性。
  6. 易于学习和掌握,对于测试操作人员而言,易于理解。
描述测试集的方法:
TTCN:

TTCN提供两种表示方法:树型记法和表型记法
树型记法主要用于描述测试事件之间的时序关系,即描述协议的动态行为。
表型记法主要用于简化所有静态数据的表示,如数据类型、PDU和ASP的格式、与测试事件相关联的测试判决等等。

上一篇 下一篇

猜你喜欢

热点阅读