论文标题
智能合同正式规格和验证的调查
A Survey of Smart Contract Formal Specification and Verification
论文作者
论文摘要
智能合约是一款计算机程序，允许用户在区块链平台上自动化其操作。鉴于智能合约在支持各个行业的重要活动（包括供应链，金融，法律和医疗服务）中具有重要意义，因此对验证和验证技术的需求很大。然而，绝大多数智能合约都缺乏任何形式规格，这对于确定其正确性至关重要。在这项调查中，我们调查了文献中介绍的智能合约的正式模型和规格，并提出了系统的概述，以了解共同的趋势。我们还讨论了当前用于验证此类财产规范的方法，并确定差距，希望能够认识到未来工作的有希望的方向。
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.
