Abstract: One of the primary objectives of ambient systems is to provide services based on the ability to interact with the environment (including objects, humans and system components). An ambient system must deal with the dynamic integration of new and unexpected elements (e.g. users or devices). To fulfil the system functions, we need to specify the ambient system and its dynamic context. In this paper, we present an elaborated formal approach to model the core concepts of context-aware systems and their dynamic reconfigurations. The approach enables a high-level of abstraction and supports building context-aware systems by providing modularity and separation of concerns. For this purpose, one, we use Milner’s standard bigraphs to model the contextual part of the context-aware system and second, we provide an extension of the Bigraphical Reactive System (BRS) to model the functional part of multi-agent system architectures (BRS-MAS). Finally, to evaluate the proposed approach, we use a Bigraphical Model Checker (BigMC) to verify safety and liveliness properties through a smart car management system case study.
