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

Simple item page
dc.contributor.authorAlqahtani, Sarra
dc.contributor.authorHe, Xinchi
dc.contributor.authorGamble, Rose
dc.contributor.authorMauricio, Papa
dc.date.accessioned2020-01-04T08:16:51Z
dc.date.available2020-01-04T08:16:51Z
dc.date.issued2020-01-07
dc.description.abstractThe 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.
dc.format.extent10 pages
dc.identifier.doi10.24251/HICSS.2020.650
dc.identifier.isbn978-0-9981331-3-3
dc.identifier.urihttp://hdl.handle.net/10125/64392
dc.language.isoeng
dc.relation.ispartofProceedings of the 53rd Hawaii International Conference on System Sciences
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0/
dc.subjectBlockchain Cases and Innovations
dc.subjectformal verification
dc.subjecthyperledger fabric
dc.subjectnusmv
dc.subjectsmart contract
dc.subjectsupply chain
dc.titleFormal Verification of Functional Requirements for Smart Contract Compositions in Supply Chain Management Systems
dc.typeConference Paper
dc.type.dcmiText

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
0522.pdf
Size:
1.51 MB
Format:
Adobe Portable Document Format
Download

Collections

Blockchain Cases and Innovations