Exploring IoT Trickle-Based Dissemination Using Timed Model-Checking and Symbolic Execution

Autor:	Arnault Lapitre, Boutheina Bannour, Pascale Le Gall
Rok vydání:	2021
Předmět:	Model checking Computational model Asynchronous communication Computer science Reachability Firmware Distributed computing Symbolic execution computer.software_genre Dissemination computer TRICKLE
Zdroj:	Networked Systems ISBN: 9783030670863 NETYS
Popis:	We focus on studying an IoT algorithm called Trickle using a formal model-based approach. The algorithm has an essential role in traffic regulation across distributed networks of wireless sensors which are part of IoT. The algorithm allows efficient dissemination of information such as critical applicative data, firmware upgrades or security fixes. In this paper, we develop timed asynchronous computational models for Trickle. We show how reachability properties can be assessed on such models using a combination of model-checking and symbolic execution implemented by the tools UPPAAL and DIVERSITY, respectively. Our experiments produce promising results on highlighting updated or outdated nodes situations during dissemination.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::3d846d3e2a04dc436fda0fca2ae8d529 https://doi.org/10.1007/978-3-030-67087-0_7 Zobrazit plný text záznamu