Service Level Agreements (SLAs) play a critical role in modern service ecosystems, formalizing commitments between providers and customers to ensure compliance with performance metrics and Quality of Service (QoS) requirements. However, the lack of standardized, user-friendly tools for defining and customizing 5G SLAs in machine-readable formats, such as XML, hinders automation and interoperability in service management. To address this challenge, we propose a formal approach based on the Event-B method to model SLA contracts and ensure their correctness and reliability. We define an incremental Event-B model that captures SLA constraints and verify their consistency using proof obligations and animation. This ensures that SLA enforcement does not alter the expected execution semantics of contracts.

Battery lifetime remains a central constraint in scaling LoRaWAN deployments across diverse IoT applications. We propose a lightweight dilated causal Convolutional Neural Network (CNN) designed to forecast per-node energy consumption with high temporal fidelity. Unlike recurrent models, our approach captures both transient spikes and long-range patterns without sequential overhead, enabling efficient edge deployment. Trained on a 12-month NS-3 simulation dataset encompassing smart lighting, environmental monitoring, waste management, and agriculture, the model achieves 96.5% forecasting accuracy with mean absolute error below 0.3, improving over SARIMA and LSTM baselines by 55% and 32% respectively. We integrate this predictor into an end-to-end energy optimization pipeline where on-device inference executes every 15 minutes with under 5 ms overhead. Forecasts drive adaptive duty-cycling, transmission slotting, and data rate control, extending device lifetime by 20%, halving collision rates, and improving fairness by 15%. Real-world validation on ten STM32F407VG microcontrollers and a commercial RAK7258 gateway confirms practical feasibility: inference completes within 0.8 ms with 4.4 mW peak power draw and 95.6% packet delivery ratio. These results demonstrate the CNN's suitability for real-time, edge-centric forecasting and its potential for enabling sustainable, intelligent LoRaWAN networks.

ABSTRACT Industrial automation and smart ecological monitoring are key fields of Internet of Things environments, where devices function under complex practical conditions and with restricted infrastructure. In such conditions, devices often face critical concerns in guaranteeing trustworthiness and better outcomes. In this article, we preliminarily suggest a thoughtful design that anticipates the programming complexities of Internet of Things (IoT) environments and accounts for their unpredictable conduct under practical conditions. Central to our strategy is the use of a method grounded in mathematical logic to allow their core properties to be rigorously checked through mathematical proofs. This process builds trustworthy IoT infrastructures and ensures dependability of their conduct before practical programming. Beyond theoretical design, we perform programming and field experiments, demonstrating that mathematically grounded designs lead directly to more productive environment outcomes, particularly in restricted conditions where infrastructure must be exploited judiciously. The results underscore the value of integrating our mathematically checked design not only at the design level but also in shaping concrete solutions for critical blockchain‐enabled IoT environments. Finally, the results show that applying our design translates into demonstrable outcomes and easier environment adaptation during practical programming.

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.

IoT-Cloud environments are being increasingly adopted for the deployment of applications and particularly resource-oriented ones. However, ensuring correct communications during the execution of IoT applications is not guaranteed. In fact, a substantial class of applications is intended to run on constrained IoT networks. Moreover, IoT devices exchange the data derived from various Cloud providers and in accordance with different protocols. In this paper, we propose a formal approach to model and verify the applications deployed over IoT-Cloud environments. The proposed model encompasses four verification levels: the Structural, Functional, Operational and Behavioral levels. Therefore, we opted for the Event-B formal method that allows gradual problems decomposition by relying on its refinement capabilities. The proposed approach has proven its efficiency for the modeling and the verification of IoT applications. We applied mathematical proof-based method to verify the model since it provides rigorous reasoning. We also employed the ProB animator to proceed in the validation of the model.

Internet of Things (IoT) is a finite set of interconnected devices that can cooperate and interact with each other through the Internet. As the number of IoT devices have increased, the number of services increased as well, further complicating the process of service composition. In this paper, an Event-B formal model is presented to verify the correctness of the IoT service composition (IoTSC) system. In addition, the proposed model satisfies some functional and non-functional properties such as compatibility and availability to fulfil the requirements of the IoTSC. Our model is developed incrementally from abstract level to target level by using the refinement mechanism. A Fire Alarm Detection System is used as a case study for our model. Finally, we use proof obligations and the Rodin platform to validate and proof the correctness of the proposed formal model.

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.

The Internet of Things (IoT) has recently taken on a crucial role in numerous areas of our life, offering convenience and efficiency. One notable area of its application is in the growing adoption of smart home applications. This rapid growth has emphasized the pressing need to enhance the IT infrastructure to ensure the transparency, security, and privacy of user data. In this regard, blockchain technology has emerged as a promising solution to fulfill these critical demands. Hence, this study suggests an approach utilizing Hyperledger Fabric to enhance the security of smart home systems through blockchain technology. The proposed solution addresses the security limitations often encountered in existing permissioned blockchain approaches. The architecture consists of four layers: Cloud Storage Layer, Blockchain Platform Layer, Application layer and IoT Devices Layer. We have integrated a cloud storage layer to take benefit of its inherent advantages in terms of efficiency and availability. Smart home devices frequently require computing resources and substantial storage capacity, both of which can be effectively provided by the cloud.

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.

Abstract Many disciplines have adopted component-based principles to avail themselves of the many advantages they bring, especially component reusability. In a short time, the component-based architecture became a renown branch in the IT world and the center of interest of many researchers. Much work has been conducted in this context for the verification of component-based applications (CBAs). However, the main focus has been on the structural aspect of such compositions, while the behavioral aspect has seldom been dealt with. In this paper, our goal is to close this gap and propose a formal approach to verify the behavioral correctness of CBAs. We first define a set of requirements to be satisfied by the structure and the behavior of a CBA, represented by a set of interactions that may occur between their components. Then, we build a formal Event-B model to represent these requirements in a rigorous and non-ambiguous way. The use of the Event-B refinement technique allows us to master the complexity of CBAs by introducing their elements in an incremental manner. The correctness of the development is ensured by establishing a set of proof obligations, under the Rodin platform, and also by animating it with the ProB animator/model checker. The approach is illustrated by a running example.

Abstract The verification of the Cloud composite services’ correctness is challenging. In fact, multiple component services, derived from different Cloud providers with different service description languages and communication protocols, are involved in the composition which may raise incompatibility issues that in turn lead to a non-consistent composition. In this work, we propose a formal approach to model and verify Cloud composite services. Four verification levels are considered in this article; the structural, semantic, behavioral, and resource allocation levels. Therefore, we opted for the Event-B formal method that enables complex problems decomposition thanks to its refinement capabilities. The proposed approach has proven its efficiency for the modelling and verification of Cloud composite services. The proposed model comprises four abstract levels with respect to the four verification axes. A proof-based approach is applied to the model’s verification. We also succeeded in the validation of the model thanks to the model animation provided by the PROB tool. The use of formal methods provides a rigorous reasoning and mathematical proofs on the correction of the model which ensures the elaboration of correct-by-construction composite services.

Abstract Cloud environments are being increasingly used for the deployment and execution of complex applications and particularly component-based ones. They are expected to provide elasticity, among other characteristics, in order to allow a deployed application to rapidly change the amount of its allocated resources in order to meet the variation in demand while ensuring a given Quality of Service (QoS). However, establishing a correct elastic component-based application is not guaranteed in Cloud. Indeed, applying elasticity mechanisms should preserve functional properties and improve non-functional properties related to QoS, performance and resource consumption. In this paper, we propose an approach for the verification and deployment of elastic component-based applications. Our approach is based on the Event-B formal method. In fact, we formally model the component artifacts using Event-B and we define the Event-B events that model the elasticity mechanisms (scaling up and down) for component-based applications. Furthermore, we formally verify that our approach preserves the semantics of the component-based applications by using the proof obligations and the ProB animator. Once the elastic component-based applications are validated, they can be deployed in a Cloud environment using an elastic deployment framework which we have developed.

With the emergence of Service Component Architecture (SCA), all interests were focused on representing this architecture in a formal way in order to be able to prevent the specifications failures. In this context, our recent works were interested in formalizing structural properties of the SCA specifications, particularly in defining structural compatibility between connected services. In fact, verifying structural compatibility is necessary but not sufficient. In this paper we intend to represent, in a first step, the SCA behavioral properties by means of Event-B invariants and events. In a second step, we established behavioral compatibility between services interacting together which is considered as a delicate task and has a great importance in guaranteeing reliable communication between services. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.

With the emergence of Service Component Architecture (SCA), all interests were focused on representing this architecture in a formal way in order to be able to prevent the specifications failures. In this context, our recent works were interested in formalising structural properties of the SCA specifications, particularly to defining structural compatibility between connected services. In fact, verifying structural compatibility is necessary but not sufficient. In this paper we intend to represent, in a first step, the SCA behavioral properties by means of Event-B invariants and events. In a second step, we established behavioral compatibility between services interacting together which is considered as a delicate task and has a great importance in guaranteeing reliable communication between services. At last, we propose an Event-B based approach so as to configure the SCA composition dynamically. We focus, particularly, on the correctional dynamic such as substituting faulty services and components. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.

Service Component Architecture (SCA) is a set of specifications which describe a model for building applications and systems using a Service-Oriented Architecture (SOA). However, SCA in its current form does not represent any formal definition. In addition, there is a growing interest for verification techniques which help to prevent SCA composition specification failure. In this context, we intend to propose an Event-B based approach so as to configure the SCA composition dynamically. We focus, particularly, on the correctional dynamic such as substituting faulty services and components. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.

Verifying Web service composition in a dynamic environment remains one of the most difficult tasks despite the efforts and the previous proposed research works because new services can be composed during the execution step and others can automatically appear, disappear, or be updated. To achieve the Web service composition specification and verification, we introduce a new concept, called dynamic pattern. A dynamic pattern is an extension of a static one. Then, we propose to formalize dynamic Web Service composition in Event-B using dynamic patterns. The resulting model is progressively verified using proofs. We use animator of model (ProB) to detect a variety of problems, such as deadlocks or other unexpected behavior of a model.