Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs

• Published in: Formal aspects of computing 2024-09, Vol.36 (3), p.1-25, Article 17
• Main Authors: Albalwe, Maram, Archibald, Blair, Sevegnani, Michele
• Format: Article
• Language: English
• Subjects: Computing methodologies; Model checking; Modeling and simulation; Models of computation; Networks; Protocol correctness; Software and its engineering; Theory of computation
• ISSN: 0934-5043; 1433-299X
• DOI: 10.1145/3685934

As more end-user applications depend on Internet of Things (IoT) technology, it is essential the networking protocols underpinning these applications are reliable. Using Formal Methods to reason about protocol specifications is an established technique, but, due to their perceived difficulty and mathematical nature, receive limited use in practice. We propose an approach based on Milner’s bigraphs—a flexible diagrammatic modelling language—that allows developers to “draw” the protocol updates as a way to increase use of formal methods in protocol design. To show bigraphs in action, we model part of the Routing Protocol for low-power and Lossy Networks (RPL), popular in wireless sensor networks, and verify it using model checking. We compare our approach with the more common simulation approach and show that analysing the bigraph model often finds more valid routes than simulation (which usually returns only a single routing tree even with 500 simulations) and that it has comparable performance. The model is open to extension, with less implementation effort than simulation, and we show this through two examples: a security attack and physical link drops. Bigraphs seem a promising approach to protocol design, and this is the first step in promoting their use.