Model Checking Intelligent Information Systems with 3-Valued Timed Commitments

Ghalya Alwhishi, Nagat Drawel, Jamal Bentahar

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

4 Scopus citations

Abstract

Intelligent Information Systems (IIS) and their applications have gained recently increasing interest in various domains. Their verification to enhance their reliability in uncertain settings constitutes a major challenge that is still attracting the research community to work on and investigate. This paper focuses on modeling and verifying IIS, taking the healthcare domain, namely a smart healthcare system as a typical example. We use the powerful concept of social conditional commitments to model the interactions among the stakeholders and capture the business logic properties of the system in the presence of uncertainty. We start by proposing 3 v- CTLcc, a new modeling language that extrapolates the two-valued timed commitment logic CTLcc to the three-value space. We define a new semantics of the commitment modality in this new logic. We also simulate and model the system and introduce a set of specifications. We verify the system model against these specifications using a model checking reduction approach. The effectiveness of the proposed approach is evaluated by implementing it on the MCMAS-SC model checker.

Original languageBritish English
Title of host publicationMobile Web and Intelligent Information Systems - 18th International Conference, MobiWIS 2022, Proceedings
EditorsIrfan Awan, Muhammad Younas, Aneta Poniszewska-Marańda
PublisherSpringer Science and Business Media Deutschland GmbH
Pages237-251
Number of pages15
ISBN (Print)9783031143908
DOIs
StatePublished - 2022
Event18th International Conference on Mobile Web and Intelligent Information Systems, MobiWIS 2022 - Virtual, Online
Duration: 22 Aug 202224 Aug 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13475 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Conference on Mobile Web and Intelligent Information Systems, MobiWIS 2022
CityVirtual, Online
Period22/08/2224/08/22

Keywords

  • 3v-Model checking
  • Conditional commitments
  • Intelligent information systems
  • Smart health system

Fingerprint

Dive into the research topics of 'Model Checking Intelligent Information Systems with 3-Valued Timed Commitments'. Together they form a unique fingerprint.

Cite this