一种代币智能合约的两段式模型检测方法 |
| |
作者姓名: | 袁政 |
| |
作者单位: | 安徽理工大学计算机科学与工程学院 安徽淮南 232001 |
| |
摘 要: | 针对代币智能合约的形式化验证方法中模型检测存在的状态空间爆炸问题,提出了一种两段式模型检测方法。使用图转换规则对智能合约建模,利用工具生成模型状态空间。第一阶段对部分状态空间进行分支时序逻辑验证后,第二阶段先使用前一阶段的状态验证信息构造马尔可夫链,使用集束搜索结合马尔可夫链对余下状态进一步筛选,再进行验证。实验结果表明,该方法能够有效减少需验证状态数量,解决状态空间问题,完成合约验证。
|
关 键 词: | 马尔可夫链 集束搜索 智能合约 形式化验证 模型检测 |
本文献已被 万方数据 等数据库收录! |
|