스마트 IoT 시스템의 신뢰성 및 안전성 검증을 위한 프로세스 대수 방법론

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

디지털 트윈 기술은 물리적 객체와 사이버 세계 간의 동적 상호작용을 가능하게 하며, 스마트 IoT 시스템의 신뢰성과 안전성을 보장하는 데 필수적이다. 그러나 기존의 IoT 통합 플랫폼은 시스템 구현에 초점이 맞춰져 있어, 스마트 IoT 시스템의 요구사항 분석과 검증에는 한계가 있다. 본 논문은 이러한 문제를 해결하기 위해 DeViLL(Delta Visual Language and Logic) 방법론을 제안한다. 이 방법론은 dTP-Calculus 프로세스 대수와 SAVE 도구 모음을 활용하여 스마트 IoT 시스템의 요구사항을 정형적으로 명세하고, 분석 및 검증한다. 또한, 이는 검증된 시스템을 openHAB 플랫폼에 통합하여 실제 환경에서의 신뢰성과 안전성을 보장한다. 본 논문에서는 스마트 홈-수영장 안전 모니터링 시스템을 설계 및 구현하는 사례 연구를 통해 DeViLL의 유효성과 실용성을 입증하였다.

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.