時艷強： 關于智能合約的形式化設計與驗證，您首次提出了驗證即服務（VaaS）的概念,并發表過一些相關的論文。為什么需要形式化驗證？如何實現驗證即服務？您可以舉一個應用場景的例子，給大家簡單介紹一下。
胡凱：回答布洛克科技【時點對話】第五問。所謂的形式化方法其實是一種驗證方法，我們平時接觸最多的是軟件測試，但實際上它只能證明軟件有錯，而不能證明軟件正確。形式化方法是解決軟件危機的另一種途徑，是一種更嚴格于軟件測試的方法，它以數學方法描述和推理為基礎，采用規范語言加形式推理，通過精確的數學手段和分析工具得到驗證。目前形式化方法是國際信息安全領域中最高級別安全軟件所強制要求的驗證方法，大體上可以分為兩類，一類叫演繹驗證，另一類叫模型檢測。
目前大多是采用模型檢測的方法驗證系統的可信性，主要過程包括模型的建立、模型的轉換、模型的驗證進行自動代碼生成，這樣的過程可以反復進行迭代。我和蔡維德教授在美國合作，在2014年提出VaaS的概念，就是驗證即服務。在這之前云服務上有很多新的理論，包括蔡維德教授提出的TaaS測試即服務理論，發表了很多相關的文章。
驗證即服務的意思是Verification as a Service，我們把驗證作為一種可以在云上提供的服務，對所有的服務可以進行按需定制、組合和驗證，并對組合服務進行驗證，這樣的驗證方式和測試方式結合，未來可以支持一些大規模的服務驗證和自動服務軟件生成，比如智能合約的微服務化、以及服務定制、組會及其驗證。
這對智能合約產生非常重要的推動作用，比如我們目前已經用SDL語言對
區塊鏈的協議進行建模，采用SDL的工具對建立的私有鏈模型進行仿真驗證，可以驗證死鎖、活鎖等一系列可信性的性質，包括功能性質和非功能的性質。我們也對智能合約采用SPIN的模型檢測工具，對智能合約進行驗證，并且實現了一些智能合約驗證的輔助工具。
【時點對話·第六問】
版權申明：本內容來自于互聯網，屬第三方匯集推薦平臺。本文的版權歸原作者所有，文章言論不代表鏈門戶的觀點，鏈門戶不承擔任何法律責任。如有侵權請聯系QQ：3341927519進行反饋。
