Modeling IoT Design Patterns Proven Correct by Construction

System architectures are becoming more complex in their understanding and analysis. Among these architectures, we find the architecture of Internet of Things (IoT). The IoT is a recent concept. It is a variety of smart objects interconnected via the internet. This variety of objects faces the problem of complexity of the system. This complexity opens the way to the use of a variety of IoT design patterns to address many issues [10]. They propose solutions for common and recurring problems to architects and designers in the IoT domain. Most of these patterns are presented visually and informally, there is no formal semantics associated with them. Hence, their meanings may be imprecise. They can lead to their misunderstanding and use.

Faced by this situation, and to remedy the problem, we propose an approach that allows to model and specify these patterns with a formal notation that allows to reuse them correctly. Our objective is to prove the relevance of these patterns. We propose an approach, allowing the formal modeling of these patterns in order to describe both their structural and behavioral features. Structural features are generally specified by the types of entities. The configuration of the entities is also described in terms of static relationships between them. Behavioral features describe successive interactions between the different entities of the IoT application. The proposed formal specification of IoT patterns is generic and it is based on the formal Event-B method. We apply our approach on different pattern examples and we illustrate it with a case study in the health care domain.

The rest of this paper is organized as follows. Section 2 discusses related works. Section 3 describes how to formally specify IoT design patterns with the Event-B method. In Sect. 4, we present an application to a case study of our approach. Section 5 concludes and gives future work directions.

Most of the proposed design patterns (Object-Oriented design patterns, Enterprise Application Integration (EAI) design patterns, Service-Oriented (SOA) design patterns, and Connected Object (IoT) design patterns) are described by a combination of a text description and a graphical representation sometimes using a proprietary notation in the aim of making them easy to understand like SOA design patterns [5] and Object Oriented design patterns [6]. However, these descriptions make patterns ambiguous and may lack details. Some work so have proposed the semi-formal representations of these patterns using modeling languages [4]. Some other works use or provide formal languages based on mathematical notation for a precise pattern specification [16]. However, these approaches require knowledge of mathematics and first order logic to use them. Some research has chosen to combine the semi-formal and formal representations of patterns. This representation ensures a better understanding and precision of patterns. Generally speaking, there is a consensus on the elements that make up and define a design pattern. However, there is no consensus on the specification of the patterns. Tounsi et al. [12, 13, 15] focused on both the modeling, the formal specification and the composition of SOA design patterns [14] and established the link between them with an automatic transformation. They used the SoaML language for the pattern modeling that ease the understanding of pattern models. For the pattern specification, they used the Event-B formal method in order to attribute formal notations to SOA design patterns for the purpose of checking their design correctness.

In this work, we are interested with the IoT design patterns. In this context we find several researchers who proposed a set of IoT design patterns in various categories. Eloranta et al. [3] proposed patterns for the construction of distributed control systems. Qanbari et al. [9] presented four patterns for the supply, deployment, orchestration and monitoring shipboard applications. Lukas et al. [10, 11] have published patterns for device power supply, operation and communication modes and a number of IoT design models. All these patterns are described with a visual and informal notation. There is no formal semantics associated. There are few numbers of research work that deals with the modeling of IoT patterns. Borelli et al. [2] proposed a language called BIoTA (Buildout IoT Application Language), to assist and streamline the building of software architectures for IoT. The specification and implementation of the BIoTA language involve a grammar and a compiler, responsible for syntax and semantic analysis, as well as code generation. This work facilitate the formalization of software architectures using automata, which would otherwise be created in an informal and ad-hoc manner but it addresses specific IoT scenarios. In this paper, we present the formal modeling of IoT patterns proposed by Reinfurt et al. [10].

Ensuring the reliability and the correctness of IoT design patterns is a goal that we have fixed. For this, we propose an approach to formally specify IoT design patterns by using the formal method Event-B that is well suited to our needs and goals. This approach allows the validation of the modeling part and ensures the verification of the relevant properties of design patterns.

Event-B is a formal method for system-level modelling and analysis [1]. It is well-suited for specifying IoT design patterns because: The primary concept in doing formal developments in Event-B is that of a model. It is made of several components of two kinds: machines and contexts. Machines contain the dynamic parts of a model, whereas contexts contain the static parts of a model. Thanks to this classification, Event-B allows the specification of structural and behavioral features of design patterns. Refinement techniques proposed by this method allow us to build patterns gradually and at different abstraction levels. Mathematical proofs allow verifying model consistency and consistency between refinement levels. The most important reason to use Event-B method is the availability of a supporting tool called the Rodin platform for modeling and automated proof [1]. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed including ones that support animation and model checking like the Prob plug-in [8] that we used.

There are two general pattern models as instances of the proposed metatamodel depending on the location of the device. If the device is placed locally, we use the “Medium Based Bootstrap Pattern” as a solution to configure the new device. If it is placed at a distance, we use the “Remote Bootstrap Pattern” as a solution.

In the specification, we concentrate on two categories of design patterns; “Bootstrapping Design Patterns” and “Registration Design Patterns”. “Bootstrapping Design Patterns” allow configuring new devices. They are composed of “Medium Based Bootstrap Pattern” and “Remote Bootstrap Pattern”. “Medium Based Bootstrap Pattern” allows to configure a new device on-site through a removable storage medium inserted in the device. This support contains the necessary information for configuration. “Remote Bootstrap Pattern” is a configuration pattern used in case that a device is placed far away and is difficult to reach. The configuration in this case is done by downloading configuration information from a bootstrap server.

“Registration Design Patterns” allow to register the attributes and the features of a new device on the Back-end server. The registration is used to facilitate the communication and the interrogation with other connected objects. There are many registration patterns. In this work, we present two patterns. So “Registration Design Patterns” are composed of “Automatic Client Driven Registration Pattern” and “Server Driven Model Pattern”. The “Automatic Client Driven Registration Pattern” allows the device to register on the Back-end server via an API call. The “Server Driven Model Pattern” is used to create a device model that includes its description and functionality.

We model structural features of design patterns with contexts in the Event-B method. They describe by a set of concepts, the structure of an IoT architecture. We use it to describe the architecture of IoT design patterns. More specifically, it is to define the entities that can be involved in the pattern, their types and their dependencies (connections). We model behavioral features of design patterns with machines in the Event-B method. We describe through this Event-B component successive interactions between the different entities of the IoT application in order to represent the two categories of the design patterns.

Smart hospitals are hospitals which build new infrastructure. In this infrastructure, all are enabled by underlying digitized networking infrastructure of interconnected assets and remote-controlled automated components which can be medical sensors, medical devices, etc. It can include several other components that can be monitored and controlled remotely to offer providers a continuous stream of real-time health data such as heart rate, blood pressure, oxygen concentration level, and glucose monitoring. Most of these components can be controlled by a mobile device or a computer. In our case study, we add a new device (a camera) to a smart hospital patient room. This device makes it possible to control the various rooms of the hospital for safety issues. For example, the camera can recognize when a patient sits up or even has a restless night’s sleep. Then it informs the nurse immediately through a notification sent to their smart phone. It can also send alerts when it detects big problems. First, the camera is added without any information to initiate its first connection. We then apply the Medium Based Bootstrap design pattern to have its configuration information. This information is inserted into the device through a memory card. Second, we go through the registration procedure on the main server (BackEndServer). This procedure is done through the use of the two patterns of the Registration Design Patterns category which are the automatic client driven registration pattern and the server driven model pattern which allow registering the device on the main server. Finally, the camera became able to communicate and create connection links with its communication partners. The camera communicates with the nurse’s smartphone to notify him of what is happening in real-time.

We model this application through the use of the model shown in Fig. 2. The camera is associated with an object of type “Device”, the memory card is defined as an object of type “Storage Medium” and the Smart phone is associated as an object of type “SmartThing”. The propagation of events between objects is done through a DeviceGateway.

In Fig. 3, we specify the static part of the design patterns of the model applied in the Smart-Hospital case study using contexts. We first specify the generic context C0. We change the generic concepts previously defined by the concepts of our case. A Camera is a Device of type object. A Smart phone is a Smart Thing of type object and a Memory card is a Storage Medium of type object. Then we specify the other contexts belonging to the Bootstrapping and the Registration patterns. In Fig. 4, we specify the dynamic aspect in the machine part of the Event-B method. We specify a part of the behavior of objects constituting the smart hospital model of our case. We describe this behavior of the configuration in the machine named BootstrappingPatterns. At the end of the specification Event-B models are proved. This case study shows that our approach is able to be applied while also taking the quality of results and performance into account.

In this paper, we presented an approach that allows to formally specify connected object architecture design patterns. In particular, specifying the “Bootstrapping Design Patterns” category and the “Registration Design Patterns” category. We formally specified these design patterns using the formal Event-B method and we described their structural and behavioral features. In our stage, we are working at a high level of abstraction, so there is no connection between the theoretical model and physical devices for machine learning. In our current work, we are working in it. The generalization of our approach is an objective that we have fixed. In previous work [7] our approach was validated with a Smart Home case study. In this paper, we applied our approach in a health care case study. As future work, we are working on applying our approach on other categories of IoT design patterns.