arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2008.02712cs.SE
收藏

智能合约形式化描述与验证研究综述

A Survey of Smart Contract Formal Specification and Verification

Palina Tolmach, Yi Li, Shang-Wei Lin, Yang Liu, Zengxiang Li

摘要:

智能合约是一种计算机程序,允许用户在区块链平台上自动执行操作。鉴于智能合约在支持包括供应链、金融、法律和医疗服务在内的各行业重要活动方面的重要性,对验证和确认技术的需求非常强烈。然而,绝大多数智能合约缺乏任何形式的规范,这对于确定其正确性至关重要。在本次调查中,我们调查了文献中提出的智能合约的正式模型和规范,并提出了一个系统的概述,以了解共同的趋势。我们还讨论了目前使用的方法,在验证这些属性的规格,并确定差距,希望认识到有前途的方向,为未来的工作。

英文摘要:

A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview in order to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑