4.6 Article

Abstracting IoT protocols using timed process algebra and SPIN model checker

出版社

SPRINGER
DOI: 10.1007/s10586-022-03963-y

关键词

IoT; Formal verification; pi calculus; Timed process algebra (TPi); SPIN model checker; PROMELA

向作者/读者索取更多资源

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.
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.

作者

我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。

评论

主要评分

4.6
评分不足

次要评分

新颖性
-
重要性
-
科学严谨性
-
评价这篇论文

推荐

暂无数据
暂无数据