{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T03:47:45Z","timestamp":1747194465475,"version":"3.40.5"},"reference-count":60,"publisher":"SAGE Publications","issue":"12","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100005632","name":"Narodowe Centrum Bada\u0144 i Rozwoju","doi-asserted-by":"publisher","award":["LIDER\/434\/L-6\/14\/NCBR\/2015"],"award-info":[{"award-number":["LIDER\/434\/L-6\/14\/NCBR\/2015"]}],"id":[{"id":"10.13039\/501100005632","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["2019\/33\/B\/ST6\/00448"],"award-info":[{"award-number":["2019\/33\/B\/ST6\/00448"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["International Journal of Distributed Sensor Networks"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:p> 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\u2013oriented 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. <\/jats:p>","DOI":"10.1177\/15501477211058667","type":"journal-article","created":{"date-parts":[[2021,12,13]],"date-time":"2021-12-13T13:19:21Z","timestamp":1639401561000},"page":"155014772110586","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Modeling and proving dynamic behaviors of a routing protocol: A tutorial"],"prefix":"10.1177","volume":"17","author":[{"given":"Agnieszka","family":"Paszkowska","sequence":"first","affiliation":[{"name":"Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Warszawa, Poland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5380-6337","authenticated-orcid":false,"given":"Konrad","family":"Iwanicki","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Warszawa, Poland"}]}],"member":"179","published-online":{"date-parts":[[2021,12,13]]},"reference":[{"volume-title":"Interconnecting smart objects with IP: the next Internet","year":"2010","author":"Vasseur JP","key":"bibr1-15501477211058667"},{"first-page":"1164","volume-title":"Proceedings of the 2018 IEEE 38th international conference on distributed computing systems (ICDCS)","author":"Iwanicki K","key":"bibr2-15501477211058667"},{"key":"bibr3-15501477211058667","doi-asserted-by":"crossref","unstructured":"Winter T, Thubert P, Brandt A, et al. RPL: IPv6 routing protocol for low-power and lossy networks (RFC 6550), 2012, https:\/\/www.rfc-editor.org\/info\/rfc6550","DOI":"10.17487\/rfc6552"},{"first-page":"406","volume-title":"Proceedings of the 9th ACM\/IEEE international conference on information processing in sensor networks (IPSN\u201910)","author":"Tsiftes N","key":"bibr4-15501477211058667"},{"volume-title":"Proceedings of the workshop on extending the Internet to low power and Lossy networks (IP+SN\u20192011)","author":"Ko JG","key":"bibr5-15501477211058667"},{"first-page":"90","volume-title":"Proceedings of the 2018 international conference on embedded wireless systems and networks (EWSN\u201918)","author":"Paszkowska A","key":"bibr6-15501477211058667"},{"first-page":"43","volume-title":"Proceedings of the 2018 14th international conference on distributed computing in sensor systems (DCOSS)","author":"Paszkowska A","key":"bibr7-15501477211058667"},{"volume-title":"Proceedings of the 15th ACM\/IEEE international conference on information processing in sensor networks (IPSN\u201916)","author":"Iwanicki K.","key":"bibr8-15501477211058667"},{"key":"bibr9-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91146-5_3"},{"volume-title":"Proceedings of the 18th annual symposium on foundations of computer science (SFCS\u20191977)","author":"Pnueli A","key":"bibr10-15501477211058667"},{"key":"bibr11-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-4129-7"},{"key":"bibr12-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15260-3"},{"key":"bibr13-15501477211058667","first-page":"411","volume-title":"Distributed systems","author":"Kopetz H","year":"1993","edition":"2"},{"first-page":"126","volume-title":"Proceedings of the 1st international conference on embedded networked sensor systems (SenSys\u201903)","author":"Levis P","key":"bibr14-15501477211058667"},{"key":"bibr15-15501477211058667","unstructured":"OMNeT++ homepage, http:\/\/www.omnetpp.org"},{"first-page":"641","volume-title":"Proceedings of the 1st international workshop on practical issues in building sensor network applications (SenseApp\u201906)","author":"Osterlind F","key":"bibr16-15501477211058667"},{"volume-title":"Proceedings of the 4th international symposium on information processing in sensor networks (IPSN\u201905)","author":"Titzer BL","key":"bibr17-15501477211058667"},{"volume-title":"Proceedings of the 4th international symposium on information processing in sensor networks (IPSN\u201905)","author":"Werner-Allen G","key":"bibr18-15501477211058667"},{"first-page":"302","volume-title":"Proceedings of the international conference on testbeds and research infrastructures for the development of networks and communities (TridentCom\u201911)","author":"Doddavenkatappa M","key":"bibr19-15501477211058667"},{"key":"bibr20-15501477211058667","unstructured":"FIT\/IoT-LAB homepage, https:\/\/www.iot-lab.info"},{"volume-title":"Proceedings of the 24th ACM international conference on modeling, analysis and simulation of wireless and mobile systems (MSWiM\u201921)","author":"Banaszek M","key":"bibr21-15501477211058667"},{"first-page":"38","volume-title":"Proceedings of the 2010 ICSE workshop on software engineering for sensor network applications (SESENA\u201910)","author":"Okola M","key":"bibr22-15501477211058667"},{"issue":"2","key":"bibr23-15501477211058667","first-page":"25","volume":"11","author":"Iwanicki K","year":"2015","journal-title":"ACM T Sensor Network"},{"volume-title":"Test-driven development: a practical guide","year":"2003","author":"Astels D.","key":"bibr24-15501477211058667"},{"volume-title":"The Rust programming language","year":"2018","author":"Klabnik S","key":"bibr25-15501477211058667"},{"first-page":"1","volume-title":"Proceedings of the ACM SIGPLAN 2003 conference on programming language design and implementation (PLDI\u201903)","author":"Gay D","key":"bibr26-15501477211058667"},{"key":"bibr27-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1145\/1274858.1274860"},{"first-page":"295","volume-title":"Proceedings of the 7th ACM conference on embedded networked sensor systems (SenSys\u201909)","author":"Burri N","key":"bibr28-15501477211058667"},{"key":"bibr29-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1002\/nem.570"},{"first-page":"121","volume-title":"Proceedings of the 2nd European workshop on wireless sensor networks (EWSN\u201905)","author":"Tolle G","key":"bibr30-15501477211058667"},{"first-page":"416","volume-title":"Proceedings of the 2006 5th international conference on information processing in sensor networks (IPSN\u201906)","author":"Whitehouse K","key":"bibr31-15501477211058667"},{"first-page":"205","volume-title":"Proceedings of the ACM embedded networked sensor systems (SenSys\u201907)","author":"Cooprider N","key":"bibr32-15501477211058667"},{"first-page":"158","volume-title":"Proceedings of the 6th international conference on information processing in sensor networks (IPSN\u201907)","author":"Archer W","key":"bibr33-15501477211058667"},{"first-page":"337","volume-title":"Proceedings of the 2009 international conference on information processing in sensor networks (IPSN\u20192009)","author":"Romer K","key":"bibr34-15501477211058667"},{"key":"bibr35-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04651-8_4"},{"first-page":"85","volume-title":"Proceedings of the 2020 international conference on embedded wireless systems and networks (EWSN\u201920)","author":"Ribeiro LB","key":"bibr36-15501477211058667"},{"key":"bibr37-15501477211058667","unstructured":"Routing over low power and Lossy networks (roll), https:\/\/datatracker.ietf.org\/wg\/roll"},{"key":"bibr38-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"bibr39-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"bibr40-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020949"},{"key":"bibr41-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"first-page":"18","volume-title":"Proceedings of the 4th USENIX conference on networked systems design and implementation (NSDI\u201907)","author":"Killian C","key":"bibr42-15501477211058667"},{"first-page":"186","volume-title":"Proceedings of the 9th ACM\/IEEE international conference on information processing in sensor networks (IPSN\u201910)","author":"Sasnauskas R","key":"bibr43-15501477211058667"},{"first-page":"174","volume-title":"Proceedings of the 9th ACM\/IEEE international conference on information processing in sensor networks (IPSN\u201910)","author":"Li P","key":"bibr44-15501477211058667"},{"first-page":"32","volume-title":"Proceedings of the 2010 ICSE workshop on software engineering for sensor network applications (SESENA\u201910)","author":"Mottola L","key":"bibr45-15501477211058667"},{"first-page":"49","volume-title":"Proceedings of the 2003 conference on applications, technologies, architectures, and protocols for computer communications (SIGCOMM\u201903)","author":"Sobrinho JL.","key":"bibr46-15501477211058667"},{"volume-title":"Proceedings of the 15th international conference on information processing in sensor networks (IPSN\u201916)","author":"Hoffmann S","key":"bibr47-15501477211058667"},{"first-page":"1","volume-title":"Proceedings of the 13th annual ACM symposium on parallel algorithms and architectures (SPAA\u201901)","author":"Thorup M","key":"bibr48-15501477211058667"},{"key":"bibr49-15501477211058667","unstructured":"Burckhardt S, Gotsman A, Yang H. Understanding eventual consistency. Technical report MSR-TR-2013-39, 2013. Microsoft Research, https:\/\/www.microsoft.com\/en-us\/research\/publication\/understanding-eventual-consistency\/"},{"key":"bibr50-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1145\/3209277"},{"key":"bibr51-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1561\/2500000011"},{"key":"bibr52-15501477211058667","unstructured":"Vasseur JP, Kim M, Pister K, et al. Routing metrics used for path calculation in low-power and lossy networks (RFC 6551), 2012, https:\/\/datatracker.ietf.org\/doc\/html\/rfc6551"},{"key":"bibr53-15501477211058667","doi-asserted-by":"crossref","unstructured":"Hui J, Vasseur JP. The routing protocol for low-power and lossy networks (RPL) option for carrying RPL information in data-plane datagrams (RFC 6553), 2012, https:\/\/datatracker.ietf.org\/doc\/html\/rfc6553","DOI":"10.17487\/rfc6553"},{"key":"bibr54-15501477211058667","doi-asserted-by":"crossref","unstructured":"Levis P, Clausen T, Hui J, et al. The trickle algorithm (RFC 6206), 2011, https:\/\/datatracker.ietf.org\/doc\/html\/rfc6206","DOI":"10.17487\/rfc6206"},{"key":"bibr55-15501477211058667","doi-asserted-by":"crossref","unstructured":"Thubert P. Objective function zero for the routing protocol for low-power and lossy networks (RPL) (RFC 6552), 2012, https:\/\/datatracker.ietf.org\/doc\/html\/rfc6552","DOI":"10.17487\/rfc6552"},{"key":"bibr56-15501477211058667","doi-asserted-by":"crossref","unstructured":"Gnawali O, Levis P. The minimum rank with hysteresis objective function (RFC 6719), 2012, https:\/\/datatracker.ietf.org\/doc\/html\/rfc6719","DOI":"10.17487\/rfc6719"},{"key":"bibr57-15501477211058667","doi-asserted-by":"crossref","unstructured":"Teraoka F, Gogo K, Mitsuya K, et al. Unified layer 2 (L2) abstractions for layer 3 (L3)-driven fast handover (RFC 5184), 2008, https:\/\/datatracker.ietf.org\/doc\/rfc5184\/","DOI":"10.17487\/rfc5184"},{"key":"bibr58-15501477211058667","doi-asserted-by":"crossref","unstructured":"Narten T, Nordmark E, Simpson W, et al. Neighbor discovery for IP version 6 (IPv6) (RFC 4861), 2007, https:\/\/datatracker.ietf.org\/doc\/html\/rfc4861","DOI":"10.17487\/rfc4861"},{"key":"bibr59-15501477211058667","first-page":"395","volume":"7","author":"Perlman R.","year":"1983","journal-title":"Comput Netw"},{"key":"bibr60-15501477211058667","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1978.1094040"}],"container-title":["International Journal of Distributed Sensor Networks"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/15501477211058667","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/15501477211058667","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/15501477211058667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,13]],"date-time":"2021-12-13T13:20:05Z","timestamp":1639401605000},"score":1,"resource":{"primary":{"URL":"http:\/\/journals.sagepub.com\/doi\/10.1177\/15501477211058667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":60,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["10.1177\/15501477211058667"],"URL":"https:\/\/doi.org\/10.1177\/15501477211058667","relation":{},"ISSN":["1550-1477","1550-1477"],"issn-type":[{"type":"print","value":"1550-1477"},{"type":"electronic","value":"1550-1477"}],"subject":[],"published":{"date-parts":[[2021,12]]}}}