Runtime Verification Tool for the Calculus of Context-Aware Ambients

François Siewe ()
Additional contact information
François Siewe: School of Computer Science and Informatics, De Montfort University, Leicester LE1 9BH, UK

Mathematics, 2025, vol. 13, issue 22, 1-40

Abstract: A context-aware system is a system that adapts its behaviours in response to changes in the system’s environment (i.e., context). Ensuring the correctness of such a system is difficult because the state of the environment changes frequently in an unpredictable manner according to the laws of physics. Hence, formal verification techniques like model-checking and theorem proving do not work in many cases. Runtime Verification (RV) is a lightweight formal verification technique that consists of checking at runtime whether the execution of the system violates the requirements of the system. The Calculus of Context-aware Ambients (CCA) is a process calculus for modelling context-aware systems and reasoning about their behaviours. This paper proposes an RV tool for CCA, called ccaRV. Given a model of a system in CCA and a property of the system written in LTL (Linear Temporal Logic), ccaRV verifies automatically at runtime if the execution of the system violates the property. We propose a semantic approach to RV, where the RV mechanism is defined at the semantics level and not as an add-on. A consequence of this is that there is no need for generating a monitor from the property specification nor for the instrumentation of a system during verification. We define a labelled reduction relation for CCA, where the labels are used to capture the execution traces at the semantics level. Then we extend LTL with spatial operators and context expressions in order to formulate properties about the system context. We use a case study of the MQTT (Message Queue Telemetry Transport) protocol to evaluate the proposed RV approach. The results show that the ccaRV tool is scalable and its decisions are accurate.

Keywords: runtime verification; linear temporal logic; process calculus; context-aware systems; calculus of context-aware ambients (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2025
References: Add references at CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/13/22/3606/pdf (application/pdf)
https://www.mdpi.com/2227-7390/13/22/3606/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:13:y:2025:i:22:p:3606-:d:1791622

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().