Page 311 - 《软件学报》2026年第5期
P. 311

2190                                                       软件学报  2026  年第  37  卷第  5  期


                 Alloy  建模了分布式协议, 如    Zave [117] 建模了 Chord 协议并发现了设计缺陷, 这表明即使是经过手写数学证明验证
                 的协议, 仍可能存在设计问题.
                    TLA+ [34] 是一种基于数学的轻量级形式化规格语言, 主要用于并发和分布式系统的描述与验证, 由 Lamport 发
                 明, 核心基于时序逻辑      (temporal logic) 和行动逻辑  (actions logic). TLA+规约使用状态-转移的状态机模型, 支持时
                 序逻辑表达    (如 eventually、always 等), 并可通过精化进行层次化建模. PlusCal     [114] 是 TLA+ 的类  Pascal/C 风格的
                 子语言, 旨在更接近命令式编程, 通过编写伪代码后转换为 TLA+ 进行验证. TLA+/PlusCal 语言简单易学, 并拥有
                 丰富的配套工具, 如 TLC     [35]  (用于模型检验) 和 TLAPM  [129]  (用于定理证明). TLC 工具成熟, 支持复杂的属性规约
                 及高效的状态约减技术, 如状态去重和对称约减等.
                    Amazon 曾调研 TLA+ 和 Alloy 在工业界应用中的适用性, 在综合考虑了建模能力、学习成本和回报比等因
                 素后, 选择了 TLA+   [22,130] , Amazon 的成功经验进一步在工业界推广了 TLA+ 的使用.
                    综合式规约语言: 综合式规约语言结合了规约语言和通用编程语言的特征, 是一种领域特定语言. 它一方面为
                 规约提供高层次的抽象框架, 并配备成熟的验证工具, 另一方面其语言风格接近传统编程语言, 减轻了开发者的学
                 习和开发成本. 基于综合式编程语言开发的规约与底层代码实现更为贴近, 有助于减少开发人员在保持一致性方
                 面的负担. 此外, 综合式规约语言还提供面向目标代码的编译工具链, 能够将规约自动编译为基于通用编程语言的
                 目标代码.
                    P 语言  [115] 是一种代表性的综合式规约语言, 主要用于分布式           (或事件驱动) 系统建模. 最初由 Microsoft Research
                 开发, P 语言为分布式系统提供了基于状态机的高层抽象框架. 它采用异步事件驱动模型, 将系统建模为一组互相
                 通信的状态机, 状态机之间通过异步方式进行交流. 与 TLA+ 等基于数学的规约语言相比, P 语言的使用体验更接
                 近传统编程语言. P 语言将正确性规约、系统行为规约和测试场景配置分开, 符合开发者的习惯, 使得规约开发和
                 维护变得更加可控. P 语言编译器可以自动将规约转译为 C、C#、Java 等语言的代码, 确保代码与规约一致. P 语
                 言已得到 Amazon、Microsoft 和  DeepSeek  等公司使用.
                    MPCal (modular PlusCal) [131] 是另一种综合式规约语言, 是 PlusCal 语言的模块化扩展. MPCal 将系统规约和环
                 境规约模块化, 从而提高了通用模块的复用性. 在规约过程中, 开发者只需分别定义系统行为、环境行为以及系统
                 的环境依赖. MPCal 的编译工具链 PGo 提供了对规约验证和代码生成的支持. PGo 不仅能将 MPCal 规约自动转
                 译为  PlusCal 代码并生成 TLA+ 供后续验证, 还能将        MPCal 规约编译为基于      Go  语言实现的可执行代码, 确保规
                 约与代码的一致性.
                    通用编程语言: 除了前述的两类规约语言外, 开发者还可以基于通用编程语言进行规约. 使用通用编程语言进
                 行规约的成本较低, 因为开发者无需专门学习特定的规约语言, 这有助于快速编写规约. 此外, 使用与系统代码相
                 同的编程语言编写的规约, 保持了与系统代码的紧密联系, 有利于规约和代码的同步演化. 然而, 在没有适合的验
                 证工具或框架支持的情况下, 基于通用编程语言的规约可能面临验证能力上的挑战.
                    在工业界, Amazon S3   团队采用    Rust 语言对其分布式键值存储节点          ShardStore 进行规约与验证   [125] . 开发团
                 队为确保轻量级和实用性         (对开发者友好), 选择了与系统实现相同的编程语言 Rust 进行规约. 团队为系统编写了
                 参考模型   (reference model), 用于定义系统的预期行为. 该参考模型的代码量约占系统实现的                 1%, 高度简洁, 并由
                 开发团队编写和维护, 确保与代码的同步演化.
                           [132]
                    Stateright  是一个面向分布式系统的       Rust 库, 设计上参考了 TLA+. Stateright 基于异步消息通信的 Actor 框
                 架构建规约, 并提供了几种可配置的网络模型, 支持指定节点崩溃次数以及不同类型的正确性性质. 此外, Stateright
                 还允许开发者自定义状态空间搜索算法, 为模型检验提供了更高的灵活性. FizzBee                       [133] 是一个面向分布式系统的
                 Python  工具, 同样参考了   TLA+的设计. FizzBee 采用  Python  语法风格, 更注重易用性和实用性, 旨在降低形式化
                 方法的学习和使用门槛, 帮助开发者在数分钟内上手进行规约编写.
                  5.2   解决模型层与代码层语义鸿沟的方法
                    交互式 DMCK 技术需要解决模型层与代码层的语义鸿沟问题, 保障二者的一致性, 才能有效地在代码中发现
   306   307   308   309   310   311   312   313   314   315   316