基于Event-B方法的区块链PBFT共识算法的形式化建模和安全性验证方法

摘要

本发明提供一种基于Event‑B方法的区块链PBFT共识算法的形式化建模和安全性验证方法，根据PBFT共识算法在区块链上的运行机制，用Event‑B建模平台Rodin实现区块链上的PBFT共识算法，对PBFT共识算法的功能安全性进行形式化验证，包括确定模型的核心元素，根据不同元素的结构及性质转换成Event‑B模型的常量和变量，对常量定义相应公理，对变量定义相应不变式保证结构和性质成立；建立抽象模型，将算法执行过程映射为具体事件；按模块进行分层精化，增加不变式对区块链的安全性质进行表示，生成证明义务，验证算法的功能安全性。本发明实现了基于模型精化技术的区块链PBFT共识算法的形式化建模，利用形式化方法对算法的功能安全性进行了验证，并支持不同区块链共识算法的精化验证。