时艳强： 关于智能合约的形式化设计与验证，您首次提出了验证即服务（VaaS）的概念,并发表过一些相关的论文。为什么需要形式化验证？如何实现验证即服务？您可以举一个应用场景的例子，给大家简单介绍一下。
胡凯：回答布洛克科技【时点对话】第五问。所谓的形式化方法其实是一种验证方法，我们平时接触最多的是软件测试，但实际上它只能证明软件有错，而不能证明软件正确。形式化方法是解决软件危机的另一种途径，是一种更严格于软件测试的方法，它以数学方法描述和推理为基础，采用规范语言加形式推理，通过精确的数学手段和分析工具得到验证。目前形式化方法是国际信息安全领域中最高级别安全软件所强制要求的验证方法，大体上可以分为两类，一类叫演绎验证，另一类叫模型检测。
目前大多是采用模型检测的方法验证系统的可信性，主要过程包括模型的建立、模型的转换、模型的验证进行自动代码生成，这样的过程可以反复进行迭代。我和蔡维德教授在美国合作，在2014年提出VaaS的概念，就是验证即服务。在这之前云服务上有很多新的理论，包括蔡维德教授提出的TaaS测试即服务理论，发表了很多相关的文章。
验证即服务的意思是Verification as a Service，我们把验证作为一种可以在云上提供的服务，对所有的服务可以进行按需定制、组合和验证，并对组合服务进行验证，这样的验证方式和测试方式结合，未来可以支持一些大规模的服务验证和自动服务软件生成，比如智能合约的微服务化、以及服务定制、组会及其验证。
这对智能合约产生非常重要的推动作用，比如我们目前已经用SDL语言对
区块链的协议进行建模，采用SDL的工具对建立的私有链模型进行仿真验证，可以验证死锁、活锁等一系列可信性的性质，包括功能性质和非功能的性质。我们也对智能合约采用SPIN的模型检测工具，对智能合约进行验证，并且实现了一些智能合约验证的辅助工具。
【时点对话·第六问】
版权申明：本内容来自于互联网，属第三方汇集推荐平台。本文的版权归原作者所有，文章言论不代表链门户的观点，链门户不承担任何法律责任。如有侵权请联系QQ：3341927519进行反馈。
