Towards a runtime verification approach for internet of things systems

Internet of Things systems are evolving at a rapid pace and their impact on our society grows every day. In this context developing IoT systems that are reliable and compliant with the requirements is of paramount importance. Unfortunately, few proposals for assuring the quality of these complex and often safety-critical systems are present in the literature. To this aim, runtime verification can be a valuable support to tackle such a complex task and to complement other software verification techniques based on static analysis and testing. This paper is a first step towards the application of runtime verification to IoT systems. In particular, we describe our approach based on a Prolog monitor, the definition of a formal specification (using trace expressions) describing the expected behaviour of the system, and the definition of appropriate input scenarios. Furthermore, we describe its application and preliminary evaluation using a simplified mobile health IoT system for the management of diabetic patients composed by sensors, actuators, Node-RED logic on the cloud, and smartphones.