Framework to Verify Distributed IoT Solutions for Traffic Analysis in ATN Stations

Abstract

IoT networks continuously evolve and require new theoretical and practical studies. Complex cooperation between IoT devices, based on interaction with their internal states especially needs to be based on new significant scientific solutions. To pursue this goal we propose a dual formalism for a distributed systems being IoT networks. We refer to it as the Integrated Model of Distributed Systems (IMDS), implemented in the Dedan framework. In this dual but integrated framework, the two views of a distributed system are available: the server view of cooperating modules or the agent view of migrating threads. The Dedan framework automatically finds deadlocks and checks distributed termination in a modeled system, observed in servers communication or in sharing resources by agents. Partial deadlocks/termination are also identified, i.e., some activities may be performed in a system that is partially deadlocked/terminated. Automated verification supports the rapid development of IoT protocols. In this paper, we also discuss the problem of how the exhaustive search in the process of deadlock detection can be improved by probabilistic search using machine learning.