Model checking real-time conditional commitment logic using transformation

Mohamed El Menshawy, Jamal Bentahar, Warda El Kholy, Amine Laarej

Research output: Contribution to journalArticlepeer-review

15 Scopus citations

Abstract

A new logical language for real-time conditional commitments called RTCTLcc has been developed by extending the CTL logic with interval bounded until modalities, conditional commitment modalities, and fulfillment modalities. RTCTLcc allows us to express qualitative and quantitative commitment requirements in a convenient way. These requirements can be used to model multi-agent systems (MASs) employed in environments that react properly and timely to events occurring at time instants or within time intervals. However, the timing requirements and behaviors of MASs need an appropriate way to scale and bundle and should be carefully analyzed to ensure their correctness, especially when agents are autonomous. In this paper, we develop transformation algorithms that are fully implemented in a new Java toolkit for automatically transforming the problem of model checking RTCTLcc into the problem of model checking RTCTL (real-time CTL). The toolkit engine is built on top of the NuSMV tool, effectively used to automatically verify and analyze the correctness of real-time distributed systems. We analyzed the time and space computational complexity of the RTCTLcc model checking problem. We proved the soundness and completeness of the transformation technique and experimentally evaluated the validity of the toolkit using a set of business scenarios. Moreover, we added a capability in the toolkit to automatically scale MASs and to bundle requirements in a parametric form. We experimentally evaluated the scalability aspect of our approach using the standard ordering protocol. We further validated the approach using an industrial case study.

Original languageBritish English
Pages (from-to)189-205
Number of pages17
JournalJournal of Systems and Software
Volume138
DOIs
StatePublished - Apr 2018

Keywords

  • Complexity
  • Qualitative and quantitative commitment requirements
  • Real-time
  • Transformation technique

Fingerprint

Dive into the research topics of 'Model checking real-time conditional commitment logic using transformation'. Together they form a unique fingerprint.

Cite this