ROS 기반 경로계획 시스템의 실시간 요구 사항 분석 = Real-time Requirements Analysis of ROS-based Path Planning Systems

국문 초록 (Abstract)

로봇 소프트웨어의 안정성과 신뢰성을 보장하기 위해 개발 단계에서 정형 검증 기법을 적용하는 노력이 증가하고 있다. 본 논문에서는 Timed Automata를 사용하여 ROS 기반의 경로계획 알고리즘을 포함한 로봇 제어 소프트웨어의 동작을 모델링하고 계산된 경로의 안전성을 모델체킹으로 정형 검증하는 방법을 제안한다. 경로의 계산 과정은 ROS2의 Data Distribution Service(DDS)가 제공하는 게시 및 구독 모델과 로봇이 주행하는 환경에 영향을 받는다. 따라서 본 논문은 경로계획 알고리즘, DDS, 동작 환경이 상호 작용하며 동작하는 통합된 모델을 제시한다. 또한 경로계획 알고리즘의 안전성(예: 충돌 회피)과 DDS를 포함한 통합 모델의 신뢰성과 같은 실시간 요구사항을 명세하고 모델체킹하는 방법을 다룬다.

다국어 초록 (Multilingual Abstract)

Efforts to apply formal verification techniques during the development stage are increasing to ensure the safety and reliability of robot software. This paper proposes a method for modeling the behavior of robot control software, specifically a ROS-based path planning algorithm, using Timed Automata. It also aims to formally verify the safety of the calculated paths through model checking. The path calculation process is influenced by the publish-and-subscribe model provided by the ROS2 Data Distribution Service (DDS) and the environment in which the robot operates. Therefore, we present an integrated model that facilitates interaction among the path planning algorithm, DDS, and the operating environment. Furthermore, this paper discusses how to specify and model-check real-time requirements, including the safety of the algorithm (e.g., collision avoidance) and the reliability of the integrated model that incorporates DDS.