Three-Valued Model Checking Smart Contract Systems with Trust Under Uncertainty

Ghalya Alwhishi, Jamal Bentahar, Ahmed Elwhishi

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

6 Scopus citations

Abstract

Blockchain systems based on smart contracts are critical systems that have to be verified in order to ensure their reliability and efficiency. Verifying these systems is a major challenge that is still an active topic of research in different domains. In this paper, we focus on verifying these systems that we model using trust protocols under uncertainty. Specifically, we address the problem using an effective verification approach called three-valued model checking. We introduce a new logic by extending the recently proposed Computation Tree Logic of Trust (TCTL) to the three-valued case (3 v- TCTL ) to reason about trust with uncertainty over smart contract-based systems. We also propose a new transformation approach to reduce the 3 v- TCTL model checking problem to the classical case. We apply our approach to a smart contract-based drug traceability system in the healthcare supply chain. The approach is implemented using a Java toolkit that automatically interacts with the NuSMV model checker. We verify this system against a set of specifications and report the results of our experiments.

Original languageBritish English
Title of host publicationThe International Conference on Deep Learning, Big Data and Blockchain, DBB 2022
EditorsIrfan Awan, Muhammad Younas, Jamal Bentahar, Salima Benbernou
PublisherSpringer Science and Business Media Deutschland GmbH
Pages119-133
Number of pages15
ISBN (Print)9783031160349
DOIs
StatePublished - 2023
Event3rd International Conference on Deep Learning, Big Data and Blockchain, DBB 2022 - Rome, Italy
Duration: 22 Aug 202224 Aug 2022

Publication series

NameLecture Notes in Networks and Systems
Volume541 LNNS
ISSN (Print)2367-3370
ISSN (Electronic)2367-3389

Conference

Conference3rd International Conference on Deep Learning, Big Data and Blockchain, DBB 2022
Country/TerritoryItaly
CityRome
Period22/08/2224/08/22

Keywords

  • Blockchain
  • Smart contract
  • TCTL
  • Three-valued model checking
  • Trust
  • Uncertainty

Fingerprint

Dive into the research topics of 'Three-Valued Model Checking Smart Contract Systems with Trust Under Uncertainty'. Together they form a unique fingerprint.

Cite this