Modeling and Verification of Context-Aware Systems

Verifying adaptive behavior is a critical challenge in the development of context-aware systems due to their complexity and uncertainty. This paper presents our novel model-based approach that provides a modeling framework to (1) specify the structural and behavioral aspects of a context-aware system, (2) define invariants of the system that need to be satisfied regardless of the adaptations, and (3) support formal verification of the system model against the invariants. Underlying this framework is our ROAD4Context model that supports the separation of adaptation concerns in context-aware systems. We show how the behavioral model of ROAD4Context can be translated into Petri nets, and how it can be verified against the system invariants. We demonstrate our approach through the modeling and verification of an adaptive cruise control system.