SaVeWoT: Scripting and Verifying Web of Things Systems and Their Effects on the Physical World

We introduce SaVeWoT (Scripting and Verifying Web of Things Systems), an approach for designing, formally verifying, and deploying decentralized control systems based on the W3C WoT. SaVeWoT consists of two main parts: the SaVeWoT language and the SaVeWoT compiler. The SaVeWoT language models devices (i.e., Things), controllers that orchestrate Things, virtual composite Things (i.e., subsystems consisting of multiple Things), interactions between these components, and their effects on the physical world. The SaVeWoT compiler uses Thing Descriptions (TDs) and SaVeWoT behavior descriptions along with correctness specifications in Linear-time Temporal Logic (LTL) to automatically generate a Promela model, which is validated using the SPIN model checker. We demonstrate the feasibility of the SaVeWoT approach by verifying a conveyor belt system as an example and conducting an empirical evaluation.