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

Boutheina Bannour (1, 2) , Arnault Lapitre (1, 2) , Pascale Le Gall (3)

1 LECS - Laboratoire Exigences et Conformité des Systèmes
2 LIMTEC (CEA, LIST) - Laboratoire Instrumentation Multi-TEChnique (CEA, LIST)
3 MICS - Mathématiques et Informatique pour la Complexité et les Systèmes

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 an original 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.

Domaines: Informatique [cs]

Boutheina Bannour, Arnault Lapitre, Pascale Le Gall. Exploring IoT Trickle-Based Dissemination Using Timed Model-Checking and Symbolic Execution. International Conference on Network Systems (NETYS), Jun 2020, Marrachech, Morocco. pp.94-111, ⟨10.1007/978-3-030-67087-0_7⟩. ⟨cea-04486240⟩