Abstracting IoT protocols using timed process algebra and SPIN model checker

The advancement of the Internet of Things (IoT) has tremendously influenced many fields of human life. The Internet of Medical Things, Internet of Flying Things, Internet of Floating Things and Internet of Autonomous Things are recent evolution of IoT. The protocols used in all forms of IoT are critical during the execution demanding formal verification methods to ensure correctness. However, the most challenging part of formal verification is abstracting the system under test, making many systems unverified. Formal protocol verification is essential for detecting specification and design flaws that go undetected and corrected during the testing phase. This paper proposes novel methods for abstracting communication patterns for IoT protocols. Message broadcasts, periodic message advertisements, topology encoding, and topology change are examples of communication patterns. An attempt is made to model these patterns using pi-calculus and PROMELA. Finally, the trickle, a wireless sensor network dissemination protocol, has been modelled using pi-calculus and PROMELA. The Spin model checker verifies design flaws, such as deadlocks and non-progress cycles. The verification results ensure that there are no deadlocks or non-progress loops. The protocol is statically verified for message transmission semantics. The analysis revealed that the protocol could only guarantee message transmission for lossy connections if an alternative route covers all other nodes. The empirical results and theorem show that the abstraction mechanism can be directly utilised for automated and theoretical verification. Researchers can use the abstraction framework described in this paper to create validation models for static and automated verification of existing and new IoT protocols.

Automated summary

The advancement of IoT has greatly impacted various aspects of human life, including the Internet of Medical Things, Internet of Flying Things, Internet of Floating Things, and Internet of Autonomous Things. Protocol verification is crucial for ensuring correctness in IoT systems, but abstracting the system under test poses a challenge. This paper proposes novel methods for abstracting communication patterns in IoT protocols, utilizing pi-calculus and PROMELA for modeling and Spin model checker for verification.