ABSTRACT During the early phases of software system development, error detection can be challenging due to the complexity of both the requirements and the operating environments. This paper advocates for the utilization of formal modelling and verification throughout the first phases of systems development to promptly detect and correct errors. The formalism employed throughout is Event‐B, which is backed by the Rodin toolset. To conquer requirements complexity, the frameworks of set theory and first‐order logic are employed, which provide the necessary tools for formalizing and analysing the properties and behaviours associated with Event‐B. Also, we detail the way in which modelling may be used to achieve abstraction, as well as the way in which refinement can be used to manage complexity through layering. Furthermore, we emphasize the significance of model validation and verification in improving the precision of formal models and requirements in IoT communication systems. The model is exemplified using a Content‐Based Publish Subscribe System (CBPS), with a special emphasis on a fire alarm system as a motivating example.

The Internet of Things (IoT) comprises a group of interconnected devices that communicate through the internet, necessitating a robust infrastructure and security protocols. Within this ecosystem, the Content-based Publish-Subscribe (CBPS) messaging paradigm enables devices to subscribe to specific data or events. However, as the number of messages transmitted increases, ensuring reliable transmission and accurate event matching becomes a challenging task. To tackle this issue, this study proposes an Event-B formal model for verifying the correctness of IoT CBPS communication. The model aims to guarantee that messages are delivered to the intended devices while ensuring the appropriate use of context information for filtering messages. Furthermore, the model's consistency has been verified using Event-B tools.

Nowadays, The Internet of Things(IoT) has shown an increased interest in the academic literature, while its implementations became involved in almost every aspect of life in modern society. IoT is the integration of virtual and physical things through distributed services to collect and share data among themselves. The number of architecture approaches designed to aid IoT has increased significantly recently. As a result of different IoT architecture approaches, in this paper, we proposed a novel correct-by-construction formal approach based on an Event-B method to describe the physical architecture of IoT layers. This formal approach inspects four layers: the physical layer, the gateway layer, the middleware layer, respectively the application layer. An Electrocardiogram (ECG) IoT system is applied in our model as a case study. Finally, we proved and validated the correctness of our formal model by using proof obligations and the model checking tool called Rodin.