Architectural Invariants and Correctness of IoT-Based Systems

Systems based on the Internet of Things impact more and more industrial areas such as smart manufacturing, smart health monitoring and home automation. Ensuring their correct construction, their well functioning and their reliability is an important issue for some of these systems which can be critical in case of dysfunction. The main requirements on physical architectures and control software are common in most of IoT-based systems. Therefore, we propose on the basis of their common architectural properties and behaviour, a generic formal model of IoT-based systems together with the rigorous analysis of their consistency properties; specific properties may be gradually added and checked. The proposed generic formal model is implemented as a parametrised model and experimented using the Event-B framework. This parametrised model is extensible; it can be profitably adapted to more general hybrid or cyber-physical systems. Moreover, our generic model is independent of the target formal modelling tools, it can be implemented in various other formal analysis environments.