1. 設(shè)計思想

針對法律、司法執(zhí)法應(yīng)用場景，將智能合約的許多問題簡化, 在智能合約的自然語言處理、形式化方法、軟件測試方面，突出智能合約的核心功能,降低使用智能合約的門檻,使其可靠且高效。

2.模型驅(qū)動開發(fā)框架

2.1 合約模板

相比將合法且有效的合同翻譯成智能合約, 本書通過領(lǐng)域分析來開發(fā)智能合約模權(quán), 提供的合約模板可以在開發(fā)過程中重復(fù)使用，且模板涵蓋某一領(lǐng)域中智能合約通用的協(xié)議條款。

eg. 契約生命周期狀態(tài)

3 原則

3.1 基于過程的原則

基于過程的原則要求律師在合同模板中定義主要權(quán)利和義務(wù)。權(quán)利和義務(wù)將是智能合約的執(zhí)行對象。

3.2. 托管原則

3.3 預(yù)言機原則

已經(jīng)通過預(yù)言機驗證過程的數(shù)據(jù)仍然可能不正確。造成錯誤的原因包括通信敗、同步錯誤或惡意攻擊。為解決這個問題, 集成數(shù)據(jù)完整性評分系統(tǒng)。幫助判定數(shù)據(jù)正確性,分?jǐn)?shù)越高越可能正確。

• 如果數(shù)據(jù)來自另一個具有完整性評分的區(qū)塊鏈,則記錄些分?jǐn)?shù)并根據(jù)區(qū)塊鏈的完整性級別調(diào)整積分;
• 如果該區(qū)塊鏈的誠信等級高,保留他的分?jǐn)?shù);如果區(qū)塊鏈誠信排名較低,積分也會降低。

3.4 共識原則

3.5 問責(zé)原則
3.6 回滾原則

4. 智能合約檢測

仿真過程中、智能合約模型在指定一組數(shù)據(jù)輸入后運行,輔助用戶確認(rèn)模型邏輯,但難以枚舉全部輸入數(shù)據(jù),因此不能保證智能合約模型完全正確,形式驗證能夠與仿真方法互補。

一般都是應(yīng)用形式化方法驗證智能合約代碼正確，驗證對象不局限于最終代碼,也包括智能合約模型,以便在設(shè)計層面提前發(fā)現(xiàn)問題。在眾多形式化驗證技術(shù)中,模型檢測較為適合驗證智能合約模型。

4.1.基于模型檢測的智能合約模型驗證

• 智能合約的控制結(jié)構(gòu)反映交易中條件分支的觸發(fā)條件及其執(zhí)行過程,交易具有確定性特點,因此智能合約系統(tǒng)的狀態(tài)空間是有限的;
• 智能合約計算復(fù)雜度較低,符合模型檢驗等技術(shù)的計算復(fù)雜度要求。eg. 利用 SPIN模型檢測工具驗證智能合約模板的正確性。

4.2.基于眾包的智能合約代碼的測試與驗證

眾包測試是軟件測試的新興趨勢,將測試任務(wù)拆分,利用眾包平臺，招聘測試人員和終端用戶參與測試任務(wù)。目前眾包測試已成功應(yīng)用在移動平臺品的可用性測試、性能測試、圖形用戶界面（GUI)測試等。

• 眾包平臺
  眾包測試驗證平臺提供通信、搜索引擎、白動化評估、自動測試、形式化驗證、事件樹分析等工具。

4.3.已有的工作使用模型檢測技術(shù)

• 使用行為交互優(yōu)先(Behavior Interaction Priority ,BIP)模型檢測工具驗證智能合約代碼、區(qū)塊鏈執(zhí)行協(xié)議和用戶行為
• 使用 Maude模型檢測工具驗證智能合約代碼的并發(fā)問題
• 使用行為交互優(yōu)先（Communicating Sequential Processes ,CSP)理論和失效—發(fā)散精化
• （Failures-Divergences Refinement, FDR)模型檢測工具驗證智能合約代碼的并發(fā)漏洞
• 使用NuSMV模型檢測工具驗證智能合約代碼(Theories , SMT)驗證智能符合需求。
• 使用可滿足性模理論(Satisfiability Modulo Theories)

參考
【1】 智能合約重構(gòu)社會契約 蔡維德 法律出版社 2020 ISBN 9787519748777.

總結(jié)

以上是生活随笔為你收集整理的智能合约重构社会契约 （5）比特犬模型实现智能合约的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。