Architectural Invariants and Correctness of IoT-based Systems

TL;DR

This paper introduces a formal framework for modeling, analyzing, and ensuring the correctness of IoT-based systems, focusing on architectural invariants and consistency to improve reliability in critical applications.

Contribution

It presents a generic, extensible formal modeling framework for IoT architectures, validated with Event-B, that ensures correctness and consistency across diverse applications.

Findings

Framework successfully models common IoT architectural properties.

Invariant properties enable rigorous analysis of system correctness.

Implementation demonstrates applicability to various formal analysis tools.

Abstract

Internet of Things applications impact more and more industrial areas such as smart manufacturing, smart health monitoring and home automation; physical objects or devices equipped with sensors and actuators are interconnected and then controlled with software applications. Ensuring the correct construction, the well-functioning and the reliability of these applications constitute important issues for some of these applications which can be critical in case of dysfunction. We propose on the basis of the formal model of their common architectural properties, a generic framework for the formal modelling of IoT-based applications, the rigorous analysis of their consistency properties, their rigorous construction and evolution. Specific properties can be gradually added and checked. The proposed framework is then implemented and experimented using Event-B. We exploit the observation that the main requirements of the IoT-based physical architectures and control software are common to all IoT-based applications; this leaded us to the definition of the generic formal model together with invariant architectural and consistency properties. The proposed approach is generic, extensible, and can be profitably adapted to more general hybrid or cyber-physical systems. Our current implementation is independent of the formal model, it can be achieved in various other formal analysis environments.