第2章 协议规范与形式化建模语言：核心概念、原理机制与实战要点

1. 问题背景：为什么协议验证必须从形式化建模开始

协议标准文档（RFC、3GPP TS、IETF Draft）通常以自然语言、状态表和报文时序图编写。这类非形式化规范在工程传递中存在三类系统性缺陷：

• 歧义性：不同实现者对同一状态迁移可能做出不同解释。
• 不可执行性：文本无法被 SPIN、NuSMV、FDR 等验证工具直接读取。
• 覆盖盲区：丢失报文、重复报文、超时重启等异常路径常被省略。

形式化建模语言以严格数学语义为协议建立可执行模型，是消除歧义、支撑自动验证的关键基础设施。这一章将建立从协议规范文本到形式化模型之间完整的知识链路。

2. 核心概念：四个最小必要概念

① 形式化模型（Formal Model）
用状态集合、事件集合和迁移关系描述协议行为，典型表示为 LTS（Labeled Transition System）：

LTS = (S, s0, Σ, δ)
S  ——状态集合  s0 ——初始状态
Σ  ——事件集合  δ ——迁移关系 δ ⊆ S × Σ × S

② 建模语言（Modeling Language）
按语义模型分为三类：进程代数（CSP、LOTOS、CCS）、扩展状态机（SDL、Statechart）、时序逻辑（TLA+、LTL/CTL）。不同语言决定模型能捕捉协议哪个维度的行为。

③ 语义映射（Semantic Mapping）
将协议原语转换为语言元素：报文类型 → 事件；连接状态 → 进程状态；定时器 → 超时迁移；丢包行为 → 非确定性选择。

④ 验证属性（Verification Property）
核心属性包括安全性（不产生错误状态）、活性（请求最终被响应）、无死锁（至少一个可执行迁移）和规范一致性。

下面以一张链路图概括形式化建模在协议验证中的位置：