Tool Supported Analysis of IoT

TL;DR

This paper presents a tool-supported approach for analyzing IoT systems by combining data flow approximation and communication soundness checks, leveraging two existing tools and an encoding strategy to enhance analysis capabilities.

Contribution

It introduces a novel method to combine data flow analysis and communication verification for IoT systems using existing tools and encoding techniques.

Findings

Combined analysis yields more comprehensive insights into IoT system behavior.

Encoding IoT-LySa into communicating machines enables integration of different analysis techniques.

The approach improves detection of communication issues in IoT systems.

Abstract

The design of IoT systems could benefit from the combination of two different analyses. We perform a first analysis to approximate how data flow across the system components, while the second analysis checks their communication soundness. We show how the combination of these two analyses yields further benefits hardly achievable by separately using each of them. We exploit two independently developed tools for the analyses. Firstly, we specify IoT systems in IoT-LySa, a simple specification language featuring asynchronous multicast communication of tuples. The values carried by the tuples are drawn from a term-algebra obtained by a parametric signature. The analysis of communication soundness is supported by ChorGram, a tool developed to verify the compatibility of communicating finite-state machines. In order to combine the analyses we implement an encoding of IoT-LySa processes into communicating machines. This encoding is not completely straightforward because IoT-LySa has multicast communications with data, while communication machines are based on point-to-point communications where only finitely many symbols can be exchanged. To highlight the benefits of our approach we appeal to a simple yet illustrative example.