Modeling and proving dynamic behaviors of a routing protocol: A tutorial
With the increasing adoption of Internet of Things technologies for controlling physical processes, their dependability becomes important. One of the fundamental functionalities on which such technologies rely for transferring information between devices is packet routing. However, while the perform...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2021-12-01
|
| Series: | International Journal of Distributed Sensor Networks |
| Online Access: | https://doi.org/10.1177/15501477211058667 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849703633439948800 |
|---|---|
| author | Agnieszka Paszkowska Konrad Iwanicki |
| author_facet | Agnieszka Paszkowska Konrad Iwanicki |
| author_sort | Agnieszka Paszkowska |
| collection | DOAJ |
| description | With the increasing adoption of Internet of Things technologies for controlling physical processes, their dependability becomes important. One of the fundamental functionalities on which such technologies rely for transferring information between devices is packet routing. However, while the performance of Internet of Things–oriented routing protocols has been widely studied experimentally, little work has been done on provable guarantees on their correctness in various scenarios. To stimulate this type of work, in this article, we give a tutorial on how such guarantees can be derived formally. Our focus is the dynamic behavior of distance-vector route maintenance in an evolving network. As a running example of a routing protocol, we employ routing protocol for low-power and lossy networks, and as the underlying formalism, a variant of linear temporal logic. By building a dedicated model of the protocol, we illustrate common problems, such as keeping complexity in control, modeling processing and communication, abstracting algorithms comprising the protocol, and dealing with open issues and external dependencies. Using the model to derive various safety and liveness guarantees for the protocol and conditions under which they hold, we demonstrate in turn a few proof techniques and the iterative nature of protocol verification, which facilitates obtaining results that are realistic and relevant in practice. |
| format | Article |
| id | doaj-art-1853656715404c2692db2daa30bcceaf |
| institution | DOAJ |
| issn | 1550-1477 |
| language | English |
| publishDate | 2021-12-01 |
| publisher | Wiley |
| record_format | Article |
| series | International Journal of Distributed Sensor Networks |
| spelling | doaj-art-1853656715404c2692db2daa30bcceaf2025-08-20T03:17:09ZengWileyInternational Journal of Distributed Sensor Networks1550-14772021-12-011710.1177/15501477211058667Modeling and proving dynamic behaviors of a routing protocol: A tutorialAgnieszka PaszkowskaKonrad IwanickiWith the increasing adoption of Internet of Things technologies for controlling physical processes, their dependability becomes important. One of the fundamental functionalities on which such technologies rely for transferring information between devices is packet routing. However, while the performance of Internet of Things–oriented routing protocols has been widely studied experimentally, little work has been done on provable guarantees on their correctness in various scenarios. To stimulate this type of work, in this article, we give a tutorial on how such guarantees can be derived formally. Our focus is the dynamic behavior of distance-vector route maintenance in an evolving network. As a running example of a routing protocol, we employ routing protocol for low-power and lossy networks, and as the underlying formalism, a variant of linear temporal logic. By building a dedicated model of the protocol, we illustrate common problems, such as keeping complexity in control, modeling processing and communication, abstracting algorithms comprising the protocol, and dealing with open issues and external dependencies. Using the model to derive various safety and liveness guarantees for the protocol and conditions under which they hold, we demonstrate in turn a few proof techniques and the iterative nature of protocol verification, which facilitates obtaining results that are realistic and relevant in practice.https://doi.org/10.1177/15501477211058667 |
| spellingShingle | Agnieszka Paszkowska Konrad Iwanicki Modeling and proving dynamic behaviors of a routing protocol: A tutorial International Journal of Distributed Sensor Networks |
| title | Modeling and proving dynamic behaviors of a routing protocol: A tutorial |
| title_full | Modeling and proving dynamic behaviors of a routing protocol: A tutorial |
| title_fullStr | Modeling and proving dynamic behaviors of a routing protocol: A tutorial |
| title_full_unstemmed | Modeling and proving dynamic behaviors of a routing protocol: A tutorial |
| title_short | Modeling and proving dynamic behaviors of a routing protocol: A tutorial |
| title_sort | modeling and proving dynamic behaviors of a routing protocol a tutorial |
| url | https://doi.org/10.1177/15501477211058667 |
| work_keys_str_mv | AT agnieszkapaszkowska modelingandprovingdynamicbehaviorsofaroutingprotocolatutorial AT konradiwanicki modelingandprovingdynamicbehaviorsofaroutingprotocolatutorial |