4. 协议状态机建模：核心概念、原理机制、实战要点

4.1 问题背景

协议规范以自然语言或 RFC 文档形式存在，缺乏精确的机器可读语义，直接交给模型检测器、定理证明器等验证工具会产生巨大鸿沟。形式化验证的“第一公里”就是为协议建立可计算、可推理的行为载体——协议状态机模型。模型质量直接决定后续验证的覆盖率、可信度和可维护性。

4.2 核心概念

• 状态（State）：协议实体在某一时刻所处的稳定模式，是变量组合或控制阶段的抽象。
• 事件（Event）：触发状态迁移的外部输入或内部信号，如报文到达、定时器超时、用户指令。
• 转换（Transition）：当前状态 + 事件 → 下一状态的迁移关系，是状态机的核心骨架。
• 守卫（Guard）：限制转换是否可用的谓词条件，如序号校验、标志位判断。
• 动作（Action）：转换发生时产生的副作用，如发送报文、更新计数器、写入变量。
• 初始状态（Initial State）：协议实例启动时所在的状态，是可达性分析的起点。

4.3 原理机制

协议状态机建模的本质，是将协议的自然语言语义转化为精确迁移系统。核心原理机制如下：

1. 状态抽象：将协议实体在任意时刻的配置、模式、标识符归并为有限个等价的离散状态。
2. 事件驱动：外部消息、定时器、内部信号统一建模为事件，驱动状态迁移。
3. 确定性约束：同一状态下同一事件至多激活一条转换，便于验证工具穷举路径。
4. 可达性分析：从初始状态出发，计算所有可到达状态，识别非法状态、死锁与不可达分支。

4.4 建模流程步骤

1. 阅读规范，提取状态集 —— 用状态命名表记录所有显式状态。
2. 识别事件集 —— 收集报文类型、定时器、用户输入等全部触发源。
3. 构建转换关系 —— 逐状态填写状态转移表，形成 δ 关系。
4. 标注守卫与动作 —— 补充谓词条件和副作用输出。
5. 模型校验 —— 检查类型正确性、无死锁、状态可达、转换完备。

4.5 案例：TCP 三次握手状态机

以 TCP 连接建立为例，服务端依赖 SYN、ACK 等事件完成状态迁移。

// 服务端状态机片段
state CLOSED:
  event LISTEN -> state LISTEN

state LISTEN:
  event SYN -> state SYN_RCVD
  action: 发送 SYN+ACK
  guard: 校验 SYN 序号合法

state SYN_RCVD:
  event ACK -> state ESTABLISHED
  guard: ACK 序号 == SYN 序号 + 1

state ESTABLISHED:
  event FIN -> state CLOSE_WAIT
  action: 发送 ACK

4.6 状态机建模要素速查表