内容

  • 学习协议验证
    • 有限状态机模型
    • Petri网模型
  • 学习示例 DLL 协议
    • HDLC
      • Frame format
    • PPP

Protocol verification 协议验证

  • 由于各种协议的复杂性，正确验证它们的正确性非常重要。
  • 验证还应确定协议中是否可能出现死锁(deadlocks)或其他问题。
  • 有几种不同的协议验证方法。
    • 有限状态机模型 -- Finite state machine models
    • Petri网模型 -- Petri net models
Finite State Machine Models
  • 每个协议机器(protocol machine)（即发送方或接收方）在每个时刻都始终处于特定状态。
    • 所有状态都表示为节点。
  • 整个系统的状态是两个协议机和通道的所有状态的组合。
    • two protocol machines and channel
  • 从每个状态，有零个或多个可能的转换(transitions )到其他状态。 当某些事件发生时会发生转换。
    • 所有过渡都表示为有向弧 -- directed arcs
  • 初始状态(Initial state)对应于系统开始运行时的描述，或在此后不久的某个方便的开始位置。
  • 可达性分析
    • 哪些状态是可达的，哪些是不可达的
    • 检测协议规范中的各种错误
  • 例子

Petri Net Models
  • Petri网有四个基本要素：places(库所), transitions（变迁）, arcs（弧）, and tokens（标记）.
    • 一个place代表系统（部分）可能处于的状态。（圆圈）
    • token指示的当前状态（粗点）
    • transition由水平或垂直条指示。
    • 每个转换都有零个或多个来自其输入位置的input arcs，以及零个或多个的output arcs，到达其输出位置。
  • 如果在每个输入位置至少有一个输入令牌，则transition可以是enabled（激活的）。
  • 任何启用的转换都可以随意fire（激发），从每个输入位置移除一个令牌并在每个输出位置存放一个令牌。
  • Petri 网可用于以类似于使用有限状态机的方式检测协议故障。
  • Petri 网可以用类似于文法的方便的代数形式（代数形式）表示。

Example DLL protocol

  • HDLC
    • High-Level Data Link Control
  • PPP
    • The Point-to-Point Protocol

HDLC

HDLC的历史

  • IBM 引入了 SDLC（同步数据链路控制）并将其提交给 ANSI 和 ISO，以作为美国和国际标准接受。
  • ANSI 将其修改为 ADCCP——高级数据通信控制程序 Advanced Data Communication Control Procedure
  • ISO 将其修改为 HDLC——高级数据链路控制 High-level Data Link Control.
  • CCITT 为其 LAP（链路访问程序）修改了 HDLC，但后来又将其修改为 LAPB。
  • 它们都非常相似，它们之间只有细微的（但令人讨厌的）差异。
帧的结构

  • 标志序列 -- Flag sequence
    • 识别帧的开始或结束
    • 位填充透明度。
  • 地址字段 -- Address field
    • 识别终端之一（在具有多个终端的线路上）
    • 区分命令和响应（对于点对点线路）
  • 控制领域 -- Control field
    • 用于序列号、确认和其他目的

Frame Types -- 帧的种类

  • Information Frame(信息帧)

  • Supervisory Frame (监控帧)

  • Unnumbered Frame (无编号帧)

  • 三种帧的Control字段的内容

Control field of

  1. An Information frame.

  2. A Supervisory frame.

  3. An Unnumbered frame.

Information Frame（信息帧）
  • Seq : N(S)
    • 发送帧序列号
  • Next : N(R)
    • 捎带确认 Piggybacked acknowledgement
    • 捎带尚未接收的第一帧的编号（即预期的下一帧），而不是正确接收的最后一帧的编号。
  • P/F
    • Poll/Final(查询/结束)
    • 当计算机轮询一组终端时使用
Supervisory Frame （监控帧）
  • Type 0 (bit3-4: 0 0) 接收就绪
    • RR帧=确认帧
    • 当没有用于搭载的反向流量时使用
  • Type 1 (bit3-4: 0 1)，如协议 5
    • RNR=否定确认帧
    • Next 字段表示未正确接收到的第一个帧
  • Type 2（位 3-4：1 0）：接收未就绪
    • 确认所有帧直到但不包括 Next
    • 告诉发件人停止发送
  • Type 3（位 3-4：1 1）：选择性拒绝
    • 只要求重传指定的帧

  • 框架结构
  • 数据字段 Data field
    • 包含任何信息
    • 可以任意长
    • 校验和的效率随着帧长度的增加而下降
  • 校验和字段 Checksum field
    • 循环冗余码 Cyclic redundancy：16bit – CRC：\(x^{16}+x^{12}+x^5+1\)

协议提供的三个命令

  • DISC (DISConnect) - 允许机器宣布它正在停机（例如，用于预防性维护）。
  • SNRM（设置正常响应模式） - 允许刚刚重新上线的机器宣布其存在并强制所有序列号归零。
    • HDLC 和 LAPB 有一个附加命令，SABM（设置异步平衡模式）。
    • SABME 和 SNRME 与 SABM 和 SNRM 相同
  • FRMR (FRaMe Reject) - 表示一个具有正确校验和但不可能语义的帧到达。

DLL in the internet

  • Point-to-Point Communication
    • Router-Router专线连接
    • 拨号主机-路由器

Point-to-Point Protocol

  • 在 RFC 1661 中定义并在其他几个 RFC（例如 RFC 1662 和 1663）中进一步详细说明。
  • PPP 提供三个特性：
    • 一种成帧方法，帧格式也处理错误检测。
    • 用于连接线路、测试线路、协商选项和关闭线路的链路控制协议。
      • 该协议称为 LCP（链路控制协议）。
    • 一种以独立于要使用的网络层协议的方式协商网络层选项的方法。 选择的方法是为每个支持的网络层使用不同的 NCP（网络控制协议）。

Typical Scenario: Connecting A Home PC To Internet Service Provider

  • 物理连接建立阶段：
    • PC 通过调制解调器呼叫提供商的路由器。
    • 路由器的调制解调器接听电话并建立物理连接。
  • 数据链路层选项协商阶段：
    • PC 在一个或多个 PPP 帧的有效载荷字段中向路由器发送一系列 LCP 数据包。 这些数据包及其响应选择要使用的 PPP 参数。
  • 网络层选项协商阶段：
    • 发送一系列 NCP 数据包以配置网络层并为 PC 分配 IP 地址（如果 PC 想要运行 TCP/IP 协议栈）。
  • 数据通信阶段：
    • PC 通过建立的连接发送和接收 IP 数据包。
  • 连接释放阶段：
    • 当PC完成后，NCP用于拆除网络层连接并释放IP地址。
    • LCP 用于关闭数据线层连接。
    • 计算机告诉调制解调器挂断电话，释放物理连接。
PPP Frame Format
  • 主要区别
    • PPP 是面向字符的，而 HDLC 是面向位的。
      • character-oriented
    • PPP 在拨号调制解调器线路上使用字节填充，因此所有帧都是整数字节。
      • byte stuffing
  • 用于无编号模式操作的 PPP 全帧格式 unnumbered mode

  • Flag -- Begin with a special byte-01111110 (same as HDLC)

    • 若封装在PPP帧中的数据出现0x7E字节，则用2字节序列0x7D、0x5E取代；
    • 若出现0x7D字节，则用2字节序列0x7D、0x5D取代；

  • Address Field --地址字段

    • 始终设置为二进制值 11111111

  • Control field -- 控制字段

    • 默认值为 00000011，表示未编号的帧。

考虑到地址和控制字段默认是不变的，所以LCP可以协商将这两个字段排除在外。

  • Protocol - 告诉 Payload 字段中的数据包类型
    • 协议字段的默认大小为 2 个字节，可以使用 LCP 协商为 1 个字节。
      • 当protocol=0x0021时，payload为IP包。
      • 当Protocol= 0xc021 时，payload为 LCP 包。
      • 当protocol=0x8021 时，payload为NCP 包。
  • Payload(有效负载) - 可变长度，最多达到一些协商的最大值，默认为 1500 字节。
  • Checksum(校验和) - 通常为 2 个字节（但可以为 4 个字节）
  • Closing flag(结束标志) – 与开始标志相同