【Author】
Tolmach, Palina; Li, Yi; Lin, Shang-Wei; Liu, Yang; Li, Zengxiang
【Source】ACM COMPUTING SURVEYS
【Abstract】A smart contract is a computer program that 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 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.
【Keywords】Smart contract; formal verification; formal specification; properties
【摘要】智能合约是一种计算机程序，允许用户在区块链平台上自动执行操作。鉴于智能合同在支持包括供应链、金融、法律和医疗服务在内的整个行业部门的重要活动方面的重要性，对验证和验证技术的需求很大。然而，绝大多数智能合约缺乏任何形式的规范，而规范对于确定其正确性至关重要。在本次调查中，我们研究了文献中提出的智能合约的正式模型和规范，并提出了一个系统的概述，以理解共同的趋势。我们还讨论了目前用于验证这些属性规格的方法，并确定差距，希望为未来的工作确定有希望的方向。
评论