Automated Transformation of IoT Systems Models into Event-B Specifications

Developing Internet of Things systems without the benefit of a standard is a difficult process. In this regard, we propose to describe Internet of Things systems using a UML meta-model. It is critical to ensure that no ambiguity, incompleteness, or misunderstanding exists in the Internet of Things systems that instantiate the meta-model. To do this, we suggest specifying Internet of Things systems by instantiating the meta-model using the Event-B formal method, which provides a starting point for architects to conduct successful verification. To do this, we suggest that conceptual modeling of Internet of Things systems be used to develop Event-B specifications. The purpose of this paper is to offer a series of both behavioral and structural transformation rules for converting each model element into its Event-B equivalent notion.