Please use this identifier to cite or link to this item: http://hdl.handle.net/10125/64392

Formal Verification of Functional Requirements for Smart Contract Compositions in Supply Chain Management Systems

File Size Format  
0522.pdf 1.55 MB Adobe PDF View/Open

Item Summary

Title:Formal Verification of Functional Requirements for Smart Contract Compositions in Supply Chain Management Systems
Authors:Alqahtani, Sarra
He, Xinchi
Gamble, Rose
Mauricio, Papa
Keywords:Blockchain Cases and Innovations
formal verification
hyperledger fabric
nusmv
smart contract
show 1 moresupply chain
show less
Date Issued:07 Jan 2020
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.
Pages/Duration:10 pages
URI:http://hdl.handle.net/10125/64392
ISBN:978-0-9981331-3-3
DOI:10.24251/HICSS.2020.650
Rights:Attribution-NonCommercial-NoDerivatives 4.0 International
https://creativecommons.org/licenses/by-nc-nd/4.0/
Appears in Collections: Blockchain Cases and Innovations


Please email libraryada-l@lists.hawaii.edu if you need this content in ADA-compliant format.

This item is licensed under a Creative Commons License Creative Commons