Verifying Timed Commitment Specifications for IoT-Cloud Systems with Uncertainty

Ghalya Alwhishi, Jamal Bentahar, Ahmed Elwhishi

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

7 Scopus citations

Abstract

Cloud Computing plays an essential role in meeting the increasing demand for large data storage and infrastructures in IoT applications. The applications of IoT-Cloud are in an exponential rise in the number of interacting components with different interaction protocols within open and uncertain environments. The main challenge that faces these applications is ensuring their reliability and efficiency. This paper proposes a scalable verification approach for IoT-Cloud applications in uncertainty-characterised settings with timed commitments using three-valued model checking. Timed commitments are powerful artifacts that capture flexible and rich interaction protocols. We use a new logic for reasoning about uncertainty in commitment protocols, model a smart contract-based IoT mortgage system with commitments under uncertain settings, introduce a set of specifications, and implement a verification framework of our model against its specifications using a transformation algorithm and the model checker. Finally, we report and discuss our experimental results.

Original languageBritish English
Title of host publicationProceedings - 2022 International Conference on Future Internet of Things and Cloud, FiCloud 2022
EditorsMuhammad Younas, Irfan Awan, Wenny Rahayu
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages173-180
Number of pages8
ISBN (Electronic)9781665493505
DOIs
StatePublished - 2022
Event9th International Conference on Future Internet of Things and Cloud, FiCloud 2022 - Rome, Italy
Duration: 22 Aug 202224 Aug 2022

Publication series

NameProceedings - 2022 International Conference on Future Internet of Things and Cloud, FiCloud 2022

Conference

Conference9th International Conference on Future Internet of Things and Cloud, FiCloud 2022
Country/TerritoryItaly
CityRome
Period22/08/2224/08/22

Keywords

  • cloud computing
  • IoT
  • model checking
  • three-valued logic
  • timed commitment logic

Fingerprint

Dive into the research topics of 'Verifying Timed Commitment Specifications for IoT-Cloud Systems with Uncertainty'. Together they form a unique fingerprint.

Cite this