A Modular Framework for Modelling and Verification of Activities in Ambient Intelligent Systems

There is a growing need to introduce and develop formal techniques for computational models capable of faithfully modelling systems of high complexity and concurrent. Such systems are the ambient intelligent systems. This article proposes an efficient framework for the automated modelling and verification of the behavioural models capturing daily activities that occur in ambient intelligent systems based on the modularity and compositionality of Petri nets. This framework consists of different stages that incorporate Petri net techniques like composition, transformation, unfolding and slicing. All these techniques facilitate the modelling and verification of the system activities under consideration by allowing the modelling in different Petri net classes and the verification of the produced models either by using model checking directly or by applying Petri net slicing to alleviate the state explosion problem that may emerge in very complex behavioural models. Illustrative examples of ambient intelligent system applied to health and other sectors are provided to demonstrate the practicality and effectiveness of the proposed approach. Finally, to show the flexibility of the proposed framework in terms of verification, both an evaluation and comparison of the state space required for the property checking are conducted with respect to the typical model checking and slicing approach respectively.