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

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

¾ IBp:当且仅当 sp = k [] I k prop []p = true ;
¾ IB¬p:当且仅当 IHp;
¾ IBP 1 ∧P 2 :当且仅当 IBP 1 并且 IBP 2 ;
¾ IBOP:当且仅当 k<j 并且(σ,k+1,j)BP;
¾ IB(P 1 ,…,P m ) prj Q:当且仅当存在 k=r 0 ≤...≤r m−1 Ur m ≤j,使得对于所有的 1≤l≤m,有(σ,r l−1 ,r l )BP l
且对于下面情况有(σ′,0,|σ′|)BP:
(1) r m <j 且σ′=σ↓(r 0 ,...,r m )⋅σ(r m+1 ,…,j);
(2) r m =j 且σ′=σ↓(r 0 ,...,r h )(其中,0≤h≤m).

1.3 UMC4M统一模型检测器
面向 MSVL 和 PPTL 的模型检测 [12] 是建立在形式化建模和形式化规约基础之上的.形式化建模采用 MSVL
程序 M 对待验证的系统进行建模,形式化规约一般采用 PPTL 逻辑公式 P 描述待验证系统需要满足的性质.由
于 MSVL 和 PPTL 均是 PTL 的子集,因此可同时将模型 M 与性质 P 统一在 PTL 框架下.验证 M→P 是否成立来
验证系统的正确性,根据逻辑公式推理可得 M→P 等价于¬(M∧¬P).在传统模型检测方法中,只需判定 M∧¬P 是
否成立便可验证性质满足性:如果公式成立,则模型违反性质;否则,模型满足性质.
UMC4M 工具对传统模型检测方法进行了改进,基础架构如图 1 所示.首先,将 PPTL 公式 P 取反,并转换为
MSVL 程序 M′;再将 MSVL 建模程序 M 与 M′合取为 MSVL 程序 M and M′,即:将(M∧¬P)是否成立转化为 M and
M′是否能够正确执行的问题;然后,通过 MSVL 编译器(MSVL compiler,简称 MC) [13] 执行 M and M′程序,并生成
+
可执行文件 M_and_M′.exe 和中间代码 MM ′ (intermediate representation);接着,通过 KLEE 处理 MM ′ 并生成
IR IR
验证用例(verification case,简称 VC);最终,运行 M_and_M′.exe 并接受 VC,然后依据执行结果判定性质是否满足.

取反
PPTL 公式 MSVL 程序 M′

MSVL 程序
M and M′
MSVL 程序 M

+
VC KLEE MM ′ IR 编译器 MC

M_and_M′.exe

满足或违反

Fig.1 Infrastructure of UMC4M
图 1 UMC4M 基础架构

2 Solidity

Solidity 是用于开发智能合约的高级语言,其语法与 Javascript 相似.相比于高级程序设计语言,Solidity 缺少
多线程以及并发等高级特性.使用 Solidity 语言编写的智能合约通过编译生成二进制字节码,并运行在以太坊虚
拟机 EVM 上.
Solidity 源文件的后缀为 sol,主要由版本标识语句、导入其他源文件以及合约的定义这 3 部分组成.其中:
版本标识语句使用保留字 pragma 声明 Solidity 的版本号,例如,pragma solidity^0.4.0,表明源文件不允许低于
0.4.0 版本的编译器编译;导入其他源文件部分使用保留字 import,相当于将多个源文件写到一个文件中,例如,
import “filename”将“filename”中所有的全局符号导入到当前全局作用域中;合约的定义部分由关键字 contract
进行声明,例如,contract{...},{…}中封装了合约,实现了合约的具体功能.
Solidity 中的合约 contract 类似面向对象高级语言中的类 Class,包含状态变量(state variables)、函数