IoT Modeling and Verification: From the CaIT Calculus to UPPAAL

With the support of emerging technologies such as 5G, machine learning, edge computing and Industry 4.0, the Internet of Things (IoT) continues to evolve and promote the construction of future networks. Existing work on IoT mainly focuses on its practical applications, but there is little research on modeling the interactions among components in IoT systems and verifying the correctness of the network deployment. Therefore, the Calculus of the Internet of Things (CaIT) has previously been proposed to formally model and reason about IoT systems. In this paper, the CaIT calculus is extended by introducing broadcast communications. For modeling convenience, we provide explicit operations to model node mobility as well as the interactions between sensors (or actuators) with the environment. To support the use of UPPAAL to verify the temporal properties of IoT networks described by the CaIT calculus, we establish a relationship between timed automata and the CaIT calculus. Using UPPAAL, we verify six temporal properties of a simple “smart home” example, including Boiler On Manually, Boiler Off Automatically, Boiler On Automatically, Lights On, Lights Mutually, and Windows Simultaneously. The verification results show that the “smart home” can work properly.