Design and Analysis of IoT Applications: A Model-Driven Approach

The Internet of Things (IoT) is a new paradigm consisting of heterogeneous entities that communicate with each other by sending and receiving messages in heterogeneous formats through heterogeneous protocols to achieve a common goal. When designing IoT applications, there are two main challenges: the complexity to represent such heterogeneous entities, message formats, and protocols in an unambiguous manner; and the lack of methodologies to verify QoS (Quality of Service) properties. This paper introduces a design and analysis process supported by a framework to assist IoT application engineers to precisely model IoT applications and verify their properties. The framework is composed of the SysML4IoT, a SysML profile based on the IoT-A Reference Model, and the SysML2NuSMV, a model-to-text translator that converts the model and QoS properties specified on it to be executed by NuSMV, a mature model checker that allows entering a system model comprising a number of communicating Finite State Machines (FSM) and automatically checks its properties specified as Computational Tree Logic (CTL) or Linear Temporal Logic (LTL) formulas. Our approach is evaluated through a proof of concept implementation that analyzes the QoS property of reliability in a Building Energy Conservation (BEC) IoT application.