Page 176 - 《软件学报》2021年第6期

1750 Journal of Software 软件学报 Vol.32, No.6, June 2021

第 8 节总结全文并讨论可能的未来工作.完整的 TLA+规约与模型检验结果参见 GitHub 仓库 [17] .

1 预备知识

1.1 TLA+简介
TLA+是由 Leslie Lamport 基于时序逻辑(temporal logic of action) [15] 开发的形式化规约语言 [13] ,尤其适合于
描述并发系统或分布式协议.
一个 TLA+规约包含一组变量、初始状态(initial state)和一组动作(action),通常表示为 Spec=Init∧[Next] vars ,
其中,vars 是所有变量的集合.状态(state)是对所有变量的赋值.Init 谓词定义了系统的初始状态,Next 是所有动作
的析取式,定义了状态之间的转换关系.[Next] vars 为真当且仅当 Next 为真(某个动作为真,即某个动作被执行)或
者所有变量的值保持不变.行为(behavior)是由状态构成的序列.TLA+使用不带撇的变量表示当前状态中变量
的值,用带撇的变量表示新状态中的值.这样,动作使用一个包含带撇变量与不带撇的变量的公式描述.例如,动
作 x′=x+1 表示变量 x 在新状态中的值比旧状态中的值大 1.
TLA+支持一阶谓词逻辑以及 ZF(zermelo-fraenkel)集合论,可以表达丰富的数据类型 [18,19] .图 1 总结了本文
用到的逻辑与集合操作符(operator).文献[20]给出了完整的 TLA+操作符列表.

Fig.1 A summary of the TLA+ operators used in this paper
图 1 本文使用的 TLA+操作符

TLA+允许 以模块 (module)的方 式进行相互 引用 . 每个模 块中 , 可以声 明常量 (CONSTANTS)与变量
(VARIABLES),定义操作符(operator)或者提出定理(THEOREM) [18,19] .一个模块可以通过扩展(EXTEND)命令来
引入其他模块中的声明、定义与定理.引入的模块可以实例化.比如,模块 M 引入了模块 M 1 .
IM 1 INSTANCE M 1 WITH p 1 ←e 1 ,…,p n ←e n ,
其中,p i 包含模块 M 1 中的所有常量与变量,e i 是由 M 中的常量与变量定义的合法表达式.该语句将 M 1 中的 p i 替
换为相应的 e i .我们可以通过 IM 1 !F 访问模块 M 1 中的表达式 F.当 e i 与 p j 相同时,TLA+的隐式替换规则允许我
[18,19]
们省略 p j ←e i .
TLC [16] 是 TLA+的模型检验工具,它可以遍历所有可能的系统行为,检查所有的状态,验证系统是否满足特