Digital twin technology enables dynamic interactions between physical objects and cyber world and is essential for ensuring the reliability and safety of Smart IoT Systems. However, the existing IoT integration platforms are focused mainly on system implementation, which limits the capability of analyzing and verifying the requirements of Smart IoT Systems in advance. To address the issue, this chapter proposes the Delta Visual Language and Logic (DeViLL) Orchestration Methodology, which utilizes formal method based on dTP-Calculus and the Specification, Analysis, Verification, Evaluation (SAVE) tool suite to formally specify, analyze, and verify the requirements. Furthermore, the verified system is integrated into the openHAB platform to ensure the reliability and safety in a real environment. The research in this chapter involves the design and implementation of a Smart Home-Pool Safety Monitoring System (SHoPoSMS) to demonstrate the validity and practicality of the DeViLL Orchestrator. The research provides a systematic approach to meet the requirements of Smart IoT Systems and reduce the risk of malfunction or misbehavior prior to the implementation. The Orchestration Methodology with DeViLL can be considered one of the most innovative approaches to utilize formal methods and tools for Smart IoT Systems on IoT integration platforms.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

DeViLL: A Methodology to Orchestrate a Formal Method and Its Tool to an IoT Integration Platform for Smart IoT Systems

  • Junsup Song,
  • Dongsu Seo,
  • Jinyoung Choi

摘要

Digital twin technology enables dynamic interactions between physical objects and cyber world and is essential for ensuring the reliability and safety of Smart IoT Systems. However, the existing IoT integration platforms are focused mainly on system implementation, which limits the capability of analyzing and verifying the requirements of Smart IoT Systems in advance. To address the issue, this chapter proposes the Delta Visual Language and Logic (DeViLL) Orchestration Methodology, which utilizes formal method based on dTP-Calculus and the Specification, Analysis, Verification, Evaluation (SAVE) tool suite to formally specify, analyze, and verify the requirements. Furthermore, the verified system is integrated into the openHAB platform to ensure the reliability and safety in a real environment. The research in this chapter involves the design and implementation of a Smart Home-Pool Safety Monitoring System (SHoPoSMS) to demonstrate the validity and practicality of the DeViLL Orchestrator. The research provides a systematic approach to meet the requirements of Smart IoT Systems and reduce the risk of malfunction or misbehavior prior to the implementation. The Orchestration Methodology with DeViLL can be considered one of the most innovative approaches to utilize formal methods and tools for Smart IoT Systems on IoT integration platforms.