Runtime Verification Tool for the Calculus of Context-Aware Ambients

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.