一种基于状态空间的智能合约形式化验证系统及方法

摘要

本发明涉及一种基于状态空间的智能合约形式化验证系统和方法，所述系统包括：代码编译模块，用于将智能合约源代码编译成源码和虚拟机操作指令字节码序列；基本块划分模块，用于将虚拟机操作指令字节码序列划分为基本块集合；控制流图生成模块，用于生成包含条件标识的控制流图；逻辑规则模块，用于将条件标识转化为逻辑规则条件；源代码形式化模块，用于从源码中解析出行为要素，保存为形式化行为文件；模型生成模块，用于根据形式化行为文件生成行为模型文件；根据逻辑规则条件和控制流图生成执行模型文件；执行与验证模块，用于获取状态空间报告和状态空间有向图。与现有技术相比，本发明具有检测全面、效率高、能直观反映出异常状态等优点。