Formal Verification of Functional Requirements for Smart Contract Compositions in Supply Chain Management Systems
Files
Date
2020-01-07
Contributor
Advisor
Department
Instructor
Depositor
Speaker
Researcher
Consultant
Interviewer
Narrator
Transcriber
Annotator
Journal Title
Journal ISSN
Volume Title
Publisher
Volume
Number/Issue
Starting Page
Ending Page
Alternative Title
Abstract
The smart contract technology has increasingly attracted the attention of different industries. However, a significant number of smart contracts deployed in practice suffer from several bugs, which enable malicious users to cause damage. The research community has shifted their focus to verifying the correctness of smart contracts using model checkers and formal verification methods. The majority of the research investigates the correctness of systems built on one smart contract. This paper proposes a verification approach for systems composed of interacting smart contracts developed and controlled by different entities. We use the NuSMV model checker and the Behavioral Interaction Priority tool to model the behaviors of smart contracts and their interactions with the aim of verifying their compliance with the systems’ functional requirements. These requirements are formalized by Linear Temporal Logic propositions. The applicability of our approach is illustrated using a case study from The American Petroleum Institute and implemented using Hyperledger Fabric.
Description
Keywords
Blockchain Cases and Innovations, formal verification, hyperledger fabric, nusmv, smart contract, supply chain
Citation
Extent
10 pages
Format
Geographic Location
Time Period
Related To
Proceedings of the 53rd Hawaii International Conference on System Sciences
Related To (URI)
Table of Contents
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International
Rights Holder
Local Contexts
Collections
Email libraryada-l@lists.hawaii.edu if you need this content in ADA-compliant format.