A Process Algebraic Methodology for Verifying Reliability and Safety of Smart IoT Systems

Digital twin technology enables dynamic interaction between physical objects and the cyber world and is essential to ensure the reliability and safety of Smart IoT System. However, existing IoT integration platforms focus on system implementation, which has limitations in analyzing and verifying the requirements of Smart IoT systems. To address the issues, this paper proposes the DeViLL (Delta Visual Language and Logic) Methodology. The methodology utilizes dTP-Calculus process algebra and the SAVE tool suite for the formal specification, analysis and verification of the requirements of Smart IoT systems. Furthermore, it integrates the verified systems into the openHAB platform to ensure their reliability and safety in real-world environments. In this paper, both effectiveness and practicality of DeViLL are demonstrated by designing and implementing a smart home-swimming pool safety monitoring system as a case study.