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