Verifying interoperability in evolving IoT systems

Abstract

As IoT devices age they must be replaced to maintain reliability and performance. During upgrades, ensuring interoperability among new and existing devices is critical for preserving designated system behaviours. Existing formal verification approaches rely on system documentation or source code to build formal models or extract flat models from system logs. We propose a novel log-driven verification framework that automatically discovers executable Hierarchical Colored Petri Nets (HCPNs) from raw IoT system logs. The framework integrates model checking to verify cross-layer interoperability during IoT system evolution and device replacement. We demonstrate the effectiveness of our approach using a street lighting system study.