基于MSVL的区块链系统建模和安全性验证的方法及系统

摘要

本发明属于形式化方法领域，公开了一种基于MSVL的区块链系统建模和安全性验证的方法及系统，在MC中用MSVL对区块链系统建模，用程序p表示；用PPTL描述区块链系统的性质，用公式φ表示；在MC中，加入MSVL的建模程序p和用PPTL描述的性质φ，验证区块链系统的安全性。本发明的区块链用MSVL程序进行建模，区块链的安全性性质用PPTL描述，而PPTL为PTL的命题子集，MSVL为PTL的可执行子集，因而MSVL和PPTL可以统一在MC中执行，相比于其他方法，本发明不需要使用另外的形式语言，也不需要调用另外的工具及大量的手工证明，只需要提供待验证性质的PPTL公式，证明过程由MC自动完成。