一种代币智能合约的两段式模型检测方法

摘要

针对代币智能合约的形式化验证方法中模型检测存在的状态空间爆炸问题,提出了一种两段式模型检测方法。使用图转换规则对智能合约建模,利用工具生成模型状态空间。第一阶段对部分状态空间进行分支时序逻辑验证后,第二阶段先使用前一阶段的状态验证信息构造马尔可夫链,使用集束搜索结合马尔可夫链对余下状态进一步筛选,再进行验证。实验结果表明,该方法能够有效减少需验证状态数量,解决状态空间问题,完成合约验证。