一種高度自動化的智能合約形式化驗證系統(tǒng)及方法

基本信息

申請?zhí)?/td> CN201810790872.0 申請日 -
公開（公告）號 CN108985073A 公開（公告）日 2018-12-11
申請公布號 CN108985073A 申請公布日 2018-12-11
分類號 G06F21/57;G06Q40/04 分類 計算；推算；計數(shù);
發(fā)明人 楊霞 申請（專利權(quán)）人 成都鏈安科技有限公司
代理機(jī)構(gòu) 成都四合天行知識產(chǎn)權(quán)代理有限公司 代理人 成都鏈安科技有限公司
地址 610000 四川省成都市成華區(qū)二環(huán)路東二段508號7層714號房
法律狀態(tài) -

摘要

摘要 本發(fā)明公開了一種高度自動化的智能合約形式化驗證系統(tǒng)及方法，包括：步驟001：將智能合約功能需求描述文檔轉(zhuǎn)換為使用非自然語言描述的智能合約功能需求規(guī)范文檔，智能合約功能需求規(guī)范文檔內(nèi)容包括目標(biāo)合約功能規(guī)范描述和安全屬性描述；步驟002：建立形式化驗證規(guī)則模型庫。步驟003：通過自動化建模工具對合約源代碼和/或字節(jié)碼進(jìn)行自動化建模；步驟004：對步驟003生成的抽象語法樹解析，為代碼中常量、變量分配內(nèi)存地址；步驟005：形式化證明。本發(fā)明適應(yīng)于多種的高級編程語言編寫的程序代碼，也適應(yīng)多種形式化語言，同時提供源代碼建模和字節(jié)碼建模兩種自動化建模方式，能夠針對用戶的不同建模需求進(jìn)行建模，進(jìn)一步提高驗證效率。