Framework to Verify Distributed IoT Solutions for Traffic Analysis in ATN Stations
Bogdan Czejdo , Wiktor B. Daszczuk
AbstractIoT 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.
|Publication size in sheets||0.6|
|Book||Zamojski Wojciech, Mazurkiewicz Jacek, Sugier Jarosław, Walkowiak Tomasz (eds.): Engineering in Dependability of Computer Systems and Networks. Proceedings of the Fourteenth International Conference on Dependability of Computer Systems DepCoS-RELCOMEX, Advances in Intelligent Systems and Computing, vol. 987, 2020, Cham, Springer, ISBN 978-3-030-19500-7, [978-3-030-19501-4 (eBook)], 554 p., DOI:10.1007/978-3-030-19501-4|
|Keywords in English||IoT negotiation protocols, Autonomous vehicles, Automated Transit Networks, ATN stations, Automated verification|
|Score||= 40.0, 10-01-2020, ChapterFromConference|
|Publication indicators||= 0|
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.