Formal modeling and verification of smart contracts

  • Xiaomin Bai
  • , Zijing Cheng
  • , Zhangbo Duan
  • , Kai Hu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Smart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an agreement on the contents of the contract and perform the contracts according to the behaviors written in certain computer algorithms. It not only needs to make sure about the correctness of smart contracts code, but also should provide a credible contract code execution environment. Blockchain provides a trusted execution and storage environment for smart contracts by the distributed secure storage, consistency verification and encryption technology. Current challenge is how to assure that smart contract can be executed as the parties’ willingness. This paper introduces formal modeling and verification in formal methods to make smart contract model and verify the properties of smart contracts. Formal methods combined with smart contracts aim to reduce the potential errors and cost during contract development process. The description of a general and formal smart contract template is provided. The tool of model checking, SPIN, is used to verify the correctness and necessary properties for a smart contract template. The research shows model checking will be useful and necessary for smart contracts.

Original languageEnglish
Title of host publicationProceedings of 2018 7th International Conference on Software and Computer Applications, ICSCA 2018
PublisherAssociation for Computing Machinery
Pages322-326
Number of pages5
ISBN (Electronic)9781450354141
DOIs
StatePublished - 8 Feb 2018
Event7th International Conference on Software and Computer Applications, ICSCA 2018 - Kuantan, Malaysia
Duration: 8 Feb 201810 Feb 2018

Publication series

NameACM International Conference Proceeding Series

Conference

Conference7th International Conference on Software and Computer Applications, ICSCA 2018
Country/TerritoryMalaysia
CityKuantan
Period8/02/1810/02/18

Keywords

  • Formal methods
  • Formal verification
  • Model checking
  • Modeling
  • SPIN
  • Smart contracts

Fingerprint

Dive into the research topics of 'Formal modeling and verification of smart contracts'. Together they form a unique fingerprint.

Cite this