Real-time Requirements Analysis of ROS-based Path Planning Systems

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