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

王小兵 等:面向 MSVL 的智能合约形式化验证 1851

(9) 下一状态赋值语句:x:=e;
(10) Always 语句:alw(p);
(11) Next 语句:next p;
(12) 循环语句:while b do p;
(13) 条件语句:if b then p else q;
(14) 投影语句:(p 1 ,…,p m ) prj q;
(15) 函数调用语句:fun(e 1 ,…,e m ).
其中,x 为变量,e 为算数表达式,b 为布尔表达式 p 1 ,…,p m ,p,q 为 MSVL 程序.
区间长度语句 empty,skip,len(n)分别声明了当前区间长度为 0,1,n;并行语句 p||q 表明 p 与 q 在当前状态下
同时开始执行,并有可能在不同时间结束;非确定选择语句 p or q 表示在当前状态下可以执行 p 或 q 中的任意一
个;顺序语句 p;q 表示 p 与 q 按照顺序执行;合取语句 p and q 表示 p 与 q 在当前状态下同时开始执行并同时结
束;等待语句 await(b)将会循环判断表达式 b 的真假,直到 b 为真时结束循环;立即赋值语句 x:=e 与下一状态赋
值语句 x<=e 分别表示在当前状态和下一状态对变量进行赋值;alw(p)表示在所有状态下执行 p; next p 表示在下
一状态执行 p; while b do p; if b then p else q 以及函数调用语句的用法与其他高级程序设计语言相同.MSVL 不
仅包含赋值语句、循环语句、条件判断语句等基本语句,还加入了框架结构和投影结构,为描述软硬件系统提
供了更强的表达能力.区间框架语句 frame(x)使得变量 x 的值能够在区间上自动遗传,否则,变量 x 仅在被赋值时
的状态下有确定的值,在其他状态下变量值是不确定的;投影语句(p 1 ,…,p m ) prj q 使得 p 1 ,…,p m 与 q 能够并行执
行,且 p 1 ,…,p m 顺序执行,而 q 在另一个状态区间上执行.
1.2 PPTL

本文描述智能合约性质使用的 PPTL 是 PTL [10] 的一个可判定子集,具有完备的公理系统 [11] ,与 MSVL 均属
于 PTL 的子集,可以共同完成对软硬件系统的形式化验证.在表达能力方面,PPTL 等价于完全正则表达式,严格
强于 LTL,能够很好地描述智能合约的性质.PPTL 的语法和语义介绍如下:
(1) PPTL 的语法
Prop 代表原子命题集合,p 代表原子命题,且 p∈Prop;P,P 1 ,…,P m 以及 Q 代表 PPTL 公式;O(next)和 prj
(projection)是 PPTL 中的时序操作符.PPTL 公式的归纳定义如下:
P,Q::=p|¬P|P∧Q|OP|(P 1 ,…,P m ) prj Q.
(2) PPTL 的语义
• PPTL 的状态:状态 s 被定义为集合 Prop 到{true,false}的一个映射关系 s:Prop→{true,false},表明一个
原子命题在状态 s 上可以为真或为假.假设命题 p 在状态 s 上的布尔值定义为 s[p],若 s[p]=true,表明是
p 在状态 s 上为真,否则为假;
• PPTL 的区间:令符号σ代表由一个或多个状态 s 组成的状态序列,即区间状态.|σ|代表区间长度,当区间
中的状态为有限个时,|σ|=状态数−1,此时,区间为有穷区间;当区间中的状态为无限个时,区间长度
|σ|=ω,此时,区间为无穷区间.为了统一有穷区间和无穷区间的表达,需要扩展非负整数集.令 N 0 代表
非负整数集,N ω 代表 N 0 ∪{ω},已知ω=ω,对于任意的 i∈N 0 ,都满足 i<ω.令U代表≤−{(ω,ω)},区间
σ=〈s 0 ,s 1 ,…,s |σ| 〉,区间σ (i−1) (0≤iUj≤|σ|)为σ的子区间.区间操作符⋅可以将两个区间σ=〈s 0 ,s 1 ,…,s |σ| 〉和
σ′ s′ 0 , ,...,s′ =〈 1 s′ | |σ 〉 连接为σ σ′ ⋅ s 0 , ,...,s 1 s ||σ , , ,...,s s′ =〈 ′ 0 1 s′ ||σ 〉 ,但前提是前一个区间σ必须为有穷区间;
• PPTL 公式的解释:令三元组 I=(σ,k,j)表示 PPTL 公式的解释,其中,σ代表区间,k 和 j 为整数且满足:
0≤kUj≤|σ|.令 P 代表一个 PPTL 公式,那么 P 的解释 I 就定义为 P 解释在σ的子区间σ(k…j)上并且在
区间上满足.这里令 I k prop 代表在状态;
• s k 上的解释,令B表示可满足关系,则公式 P 与解释 I 的可满足关系如下: