Tool Supported Analysis of IoT

Chiara Bodei
(Dipartimento di Informatica, Università di Pisa)
Pierpaolo Degano
(Dipartimento di Informatica, Università di Pisa)
Letterio Galletta
(Dipartimento di Informatica, Università di Pisa)
Emilio Tuosto
(Department of Informatics, University of Leicester)

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.

In Massimo Bartoletti, Laura Bocchi, Ludovic Henrio and Sophia Knight: Proceedings 10th Interaction and Concurrency Experience (ICE 2017), Neuchâtel, Switzerland, 21-22nd June 2017, Electronic Proceedings in Theoretical Computer Science 261, pp. 37–56.
Published: 29th November 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: