Toward a Reliable IoT Communication Protocol: UPPAAL-Verified Timed Automata for CoAP

Abstract

In our world, the Internet of Things (IoT) has long been deeply embedded in daily life, linking devices across domains as varied as healthcare, transportation, and smart homes. This interconnected world relies on lightweight communication protocols to operate under tight energy and resource constraints. Among them, the Constrained Application Protocol (CoAP) stands out for its simplicity and HTTP-like semantics—yet questions remain about its reliability and efficiency at scale and on lossy networks.

In this work, we build a formal model of CoAP using timed automata in UPPAAL [2]. The model captures key aspects of the protocol—confirmable and non-confirmable messages, acknowledgments, retransmissions, timeout management, and token/MID correlation—and is intended first for validation of functional correctness (safety, liveness, reachability). To expose timing effects without altering endpoint logic, we compose the client and server with a minimal network template. Beyond the core specification [1], we design extension hooks to broaden validation and later evaluation: Observe for notification ordering and cancel safety [3], Block-Wise transfers for block progression and reassembly completeness [4], and Hop-Limit for loop-freedom via strict hop decrement and reset on exhaustion [5].  Our study not only delivers a validated formal model of CoAP but also illuminates its strengths, limitations, and opportunities for refinement, paving the way toward more scalable and reliable IoT communication.