3 协议模型技术.ppt

1、1、第3章协议模型技术，3.1引言协议模型技术是协议工程的核心技术之一。它是协议工程的基础。形式描述语言总是基于某种模型。必须对某些模型技术进行协议正确性验证。协议自动化和协议测试性能分析基于某种模型技术。在第三章协议模型技术中，N层协议的全局系统由多个本地系统(协议实体)和(N-1)层信道组成。模型技术旨在准确描述(N-1)层信道、N层局部系统和全局系统的行为和性质。由于N层本地系统由各种协议元素组成，模型技术还必须准确描述各种协议元素的属性和行为，以及它们之间的交互关系(协议机制)。首先，研究了(N-1)层信道、N层全局系统以及协议元素的性质和行为特征。3.第三章：协议模型技术。3.1.1

2、协议的性质是指一个好的协议应该具有的性质：它包括四个主要方面：活动性、安全性、一致性和完整性。1协议的活动性(协议回归)是指协议运行时会发生一些预定的事件，会达到规定的协议状态，会执行应该执行的协议动作。协议的活动体现在两个方面：终止和进展。(1)终止：指协议从任何状态开始，始终正确到达终止状态。(2)渐进性：它意味着协议从初始状态开始运行，并且总是能够正确地到达指定状态。在某些情况下，结束状态和初始状态是相同的。这样，从初始状态运行总是可以正确地返回到初始状态，并且协议的回归可以重复运行。因此，回归=终止进展=活动。第四章，协议模型技术，可以从事件状态表中观察协议的活动。其中s是状态，I是输

3、入事件，o是输出事件。O1I2O2I1O3I3，事件状态表，状态机图，5，第3章协议模型技术，2。安全性安全性意味着当协议运行时不会发生不好的事情。这些不好的事情包括不可接受的事件。无法继续前进的状态、错误的行为、错误的条件、变量值超出界限等。坏事通常会导致两种情况：死锁和活锁。从图(a)中观察死锁和活锁现象。(死锁意味着协议在某种状态下被阻塞，而活锁意味着协议进行了无意义的循环。)假设O1I2不能保证I2(坏事发生)将在系统外发生，S0将在接收到I1后永远停留在S1。除非再次输入I3，否则无法将其返回到S0(发生死锁)。如果在S3接收I3后采取的措施发生变化(当系统状态变为S0时，I1输出，

4、即条件变为I1/o1)，则系统将在S0、S1和S3之间无休止地循环。(活锁发生)。如果在协议设计中考虑到各种“坏事”，死锁是可以避免的。安全性是可以保证的。“坏事”变成“预定的事情”或“好事”，6。第三章协议模型技术。一致性(从服务的角度)协议一致性是指协议服务行为(性质)与协议行为(性质)是一致的(服务行为：与服务原语相关；协议行为与分组数据单元及其时序相关)。N层协议用户所请求的服务和他所能观察到的服务性质与N层协议内部机制的整体行为和性质是一致的。那么协议是一致的。一致性包括两个方面：协议应该提供用户所需的服务；该协议不需要提供用户不需要的服务。7，第3章协议模型技术，4完整性(从协议的

5、可靠性和完整性方面来看)完整性意味着协议的性质完全满足协议环境的各种要求。也就是说，协议的构造考虑了诸如用户需求、用户特征、信道属性、工作模式等潜在因素的影响。并考虑对各种错误操作和异常情况的处理。5.关于协议的性质有许多说法，其中常见的有：协议的性质可以分为一般性质和特殊性质。一般属性包括：特殊属性包括一致性和完整性。协议测试侧重于特殊性验证。一致性、部分正确性和等价性是一个意思。完整性和完全正确性是一个意思。8.第3章协议模型技术，3.1.2协议元素属性许多协议元素对协议模型技术有重要影响，这里列出了其中一些。1.事件成对事件分为通信事件(外部事件)和内部事件。通信事件成对发生，而内部事件

6、(如超时)不会。例如，由N层用户发送的服务原语(输出事件)和由N层协议接收的服务原语(输入事件)成对出现在(N)个SAP的两侧，(N)个SAP是事件发生点。在另一个例子中，由N层协议实体A发送的分组数据单元和由B接收的分组数据单元是一对通信事件，它们出现在两个(n-1)SAP上，即，在两个不同的事件发生点。通信事件可以分为两类：同步事件(sync.event)和异步事件(async.event)。同步事件：输入事件和输出事件发生在同一个事件点，同时出现。异步事件：输入事件和输出事件发生在两个事件点，它们不会同时发生，输出事件落后于输入事件。9，第3章协议模型技术，2。事件的原子化无论通信事件或

7、内部事件是否发生，一旦发生，就必须完成，这就是所谓的事件的原子性。原子事件被称为原子事件。(原子事件)例如，当N层协议实体向(n-1)层信道输出消息时，一旦开始输出，即使输出失败，事件“Output Message”也被认为已经发生，并且输出失败被认为是信道丢失消息。这本书假设所有事件都是原子的。3.事件时序第二章指出服务原语的状态图表达了服务原语之间的时序关系。分组数据单元交换规则表达了分组数据单元的时序关系。因为通信事件是由服务原语和协议数据单元的交换引起的，所以它们进一步决定了通信事件的时间顺序。10.第三章协议模型技术。4.国家计时。事件定时决定状态定时，因为事件可以触发状态改变。5.

8、变量的有界性。协议变量范围的明确定义称为变量的有界性。6进程的原子性一个协议进程可以包括多个协议动作。一旦该过程开始，所有包含的动作都一次性完成，而不经过中间协议状态。没有被其他进程完全中断，这个属性被称为进程的原子性。原子过程被称为原子过程。当(原子过程)协议运行时，它从一个状态到另一个状态的转换可以被视为一个原子过程。11，第3章协议模型技术，3.1.3通道类别1。空通道：传输时间和延迟时间为0的通道。“空”的意思是通道在任何时候都不容纳消息，或者消息一从输入端进入就出现在输出端。2.非缓冲通道：在任何时候，最多只有一个通道可以传输消息。3.缓冲通道：允许多个消息停留的通道被用作缓冲通道。

9、12，第3章：协议模型技术。信道的两端是通信事件的发生点。当消息从信道的一端传输到另一端时，两个事件点产生四个事件。如果我们将两个端点标记为A和B，并假设消息是从A发送到B的，那么这四个事件的含义是：(1)a！甲端的用户向频道甲端发送一条消息，“啊！”说送，一说一结束，米说留言。(2)a？信道接收到来自终端的消息，并开始传输表示收到。(3)b！m:信道完成消息传输，并将消息发送给B端用户。(4)b？m:b终端用户从b点接收消息。13，第三章协议模型技术，一！m和a？m是一个协作事件，b！m和b？m是一个协作事件，而a！m和b？m和a？m和b！m是一个异步事件。如果消息延迟时间和传输时间之和是t

10、秒，那么a？m比b晚！m为T秒，因为空通道T=0，此时a！m和b？m和a？m和b！m也可以被视为同步事件。基于同步通信概念的模型技术或形式描述语言(如LOTOS)将通道处理成独立的进程(或事件)，而基于异步通信的模型技术形式描述语言(如ESTELLE)不需要这样做。信道：单工，半双工和全双工信道，14。第三章协议模型技术，3.1.4协议模型的选择目前，协议工程中使用的所有模型技术都来自数学家和计算机科学理论家提出的一些数学模型(或方法)和自动机模型(或程序模型)。模型技术是一种理想的模型技术，它能够方便、全面地表达协议元素和通道的各种属性(p22)，并且能够方便地观察协议属性。“方便、充分的表

11、示”意味着所采用的模型技术具有很强的表达能力和实用性。“易于观察”意味着协议验证和测试易于实施。第15章，协议模型技术，3.2有限状态机的定义：它是一个四进制系统。(1)S是系统状态集。由于状态数有限，所以称之为有限状态机。无限状态机被称为图灵机。(2)i是系统is的初始状态。(3)E是原子事件集，(4)T是状态转移函数集。转换函数被定义为如果系统处于状态S1，如果存在事件E，则系统状态变为SJ、16。第三章协议模型技术，有限状态机可以用于协议模型技术。(1)首先，它可以表达最重要的协议元素(状态和事件)的时序以及状态和事件之间的关系。此外，有限状态机具有直观和易于理解的优点。本文采用了佩森的

12、图形表示法。(2)圆圈代表状态，圆圈中的符号代表状态含义。(3)弧：带箭头的有向弧表示状态转换。弧线标记表示事件(3)黑点圆圈：中间有黑点的圆圈表示初始状态(4)方框：表示系统的边界，框架上的小圆圈表示事件发生点(或系统与外界的耦合点)。17.第三章协议模型技术3.2.2信道有限状态机三种类型的信道有限状态机有很大的区别。空通道和空通道有1个状态号，即只有真空通道不存在，但有时无缓冲通道可以转换成空通道图(b)和(d)，它们是空通道的有限状态机图。18.第3章协议模型技术，2个无缓冲信道如果在一个方向上传输的消息是相同的，那么单工无缓冲信道的状态号是2，半双工状态是3，而全双工信道的状态号是4

13、(两个单工合成)，无缓冲半双工。如果所有消息都相同，队列边界为n的单工缓冲通道的状态号为(n 1)。“队列边界”表示通道中缓冲队列的最大允许长度，表示通道是有界的。对于全双工信道，状态号为(n 1)2。20，第3章协议模型技术，在许多情况下，信道中的消息不能被认为是相同的(例如，当实现序列控制时，m个消息具有m个不同的序列号)。如果信道中有多个不同的消息(每个消息只有一个，并且消息是有序的)，那么具有边界N的单工信道的状态号如下，这表明具有边界条件2的可靠单工缓冲信道的状态号是21。第三章，协议模型技术，状态机模型如下。状态：初始状态，信道中没有消息。1状态：信道中只有消息m0；2状态：信道中

14、只有消息m1；3状态：信道中有m0和m1消息，22，第3章协议模型技术，3.2.3介绍FSM AB(Alternative Bit)协议系统，AB协议是最早的端到端通信协议之一，它经常作为协议分析的例子出现在学术论文中，其协议机制描述如下(AB协议有许多变体，本文给出其中一个：假设：1 .1:AB协议使用的信道是永不中断的全双工信道；2.消息可能在信道中丢失，并且消息内容可能是错误的，但是重复发送消息n次是正确的，至少一次；3.承认信息不会丢失、错误或重复。，23，第3章协议模型技术，发送方：发送方协议实体从发送方用户处获取消息，将序列号寄存器的值分配给消息，然后将消息发送给接收方协议实体。在

15、消息发送后启动超时时钟，并等待消息被确认。如果在给定时间内没有收到确认消息，请重新发送消息。如果收到确认消息，其序列号值与发送消息的序列号值相同，序列号寄存器的内容根据模2增加1。然后发送方实体从发送方用户获得下一条消息。24，第3章协议模型技术，接收方：收到报文后，如果报文无误，且序列号和序列号寄存器的值相等，则向发送方实体发送确认报文(确认报文的序列号值等于接收报文的序列号值等于接收报文的序列号值)，然后将报文发送给接收方用户，序列号寄存器的内容将根据模2增加1。如果收到的消息有错误或序列号不正确，它将被丢弃。25，第3章，协议模型技术，以AB协议系统为例，说明如何用有限状态机表示协议实体

16、。下图显示了AB协议系统，其中s和r是协议实体，s是发送协议实体，r是接收协议实体。a和B是AB协议系统及其用户的耦合点，相当于开放系统互连模型的SAP。它使用的通道ch是一个全双工无缓冲通道，其端点是a和b。s和r状态的含义如下：26。第3章，协议模型技术，状态1。s已从a接收到消息，序列号设置为0，消息名为m0。2.s已将m0发送给a，等待R的ack0.3.s已从a接收到消息，序列号更改为1，消息名称为m1。4.s已将m1发送到a，等待r. R状态1的ack1。r已从b. 2收到消息m0。R已向b发送ack0，R已从b. 4收到消息m1。r向B .发送了ack1，27，第3章协议模型技术，

17、FSM图的，s，FSM图的r，B，A，B，A，28，第3章协议模型技术，除正常通信事件外，系统还有两个内部事件，drop和t，drop表示一个消息错误事件，并丢弃该消息；t表示超时事件。s发出一条消息，如果在给定时间内没有收到ack消息，超时事件使他返回状态1(或3)，并重新发送m0(或m1)。对于r，如果在接收m0或m1后消息中有错误，则消息被丢弃，状态返回初始状态。如果消息正确，向用户发送ack0(ack1)消息。29，第3章协议模型技术，3.2.4有限状态机的简化状态爆炸是有限状态机面临的一个严重问题。队列边界为n的系统的有限状态机随着n的增加而迅速增加.具有x和y状态号的两个状态机被合并，状态号是XY。因此，必须研究有限状态机的简化。有限状态机的简化实际上是状态数量的减少。方法1:状态层次结构分阶段组织几个协议功能(见2.2.4)，设置状态，然后分阶段设置子状态，这样可以大大减少每个阶段的状态数量。例如，国际标准化组织的T层协议建立了22个一般状态，数据传输阶段是开放状态(第2.4.5节)。事实上，在数据传输阶段，协议包括许多子状态。当只考虑诸如连接建立和撤销的协议功能时，定义总共22个状态就足够了。30，第3章协议模型