Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

로봇 공학의 세계에서, 움직이고 생각하는 단 하나의 기계를 만드는 것도 충분히 어려운 일입니다. 하지만 서로 충돌하지 않고 협력하는 로봇 팀을 구축하는 것은 전혀 다른 차원의 도전입니다. 흔히 자율 이동 로봇(autonomous mobile robots)이라 불리는 이 기계들은 벽, 사람, 그리고 서로를 피하며 특정 목적지에 도달하도록 설계되었습니다. 이들을 구동하는 소프트웨어는 매우 복잡하며, 자신이 어디에 있고 주변에 무엇이 있는지 이해하기 위해 레이저와 같은 센서로부터 들어오는 끊임적인 데이터 스트림에 의존합니다. 이 로봇들은 연속적인 물리적 세계에서 작동하기 때문에, 그 움직임은 수 밀리미터의 거리와 수만 분의 1초 단위로 변하며 매우 부드럽고 유연합니다. 그러나 이들을 제어하는 컴퓨터는 이산적인 단계(discrete steps)로 생각하며, 정보를 뚜렷한 시간 덩어리로 처리합니다. 이 물리적 현실의 매끄러움과 코드의 단계별 논리 사이의 간극은 위험한 사각지대를 만듭니다. 만약 소프트웨어가 완벽하게 조정되지 않는다면, 로봇은 센서가 장애물을 포착하기에 너무 빠르게 움직일 수도 있고, 두 대의 로봇이 정확히 같은 순간에 교차로에 도착하여 어느 쪽도 움직일 수 없는 교착 상태(deadlock)에 빠질 수도 있습니다.

이를 해결하기 위해 연구자들은 실제 기계를 켜기 전에 로봇 팀이 직면할 수 있는 모든 가능한 시나리오를 테스트할 방법을 찾아야 합니다. 여기서 '형식 검증(formal verification)'이라는 분야가 등장합니다. 단순히 시뮬레이션을 몇 번 실행하고 운 좋기를 바라는 대신, 형식 검증은 수학적 논리를 사용하여 시스템이 취할 수 있는 모든 경로를 확인합니다. 이는 단순하지만 강력한 질문을 던집니다. "아무리 희박한 확률이라도 시스템을 실패하게 만드는 가능한 사건의 순열이 존재하는가?" 로봇 팀의 경우, 이는 그들이 결코 충돌하지 않고, 영원히 갇혀 있지 않으며, 항상 목표에 도달할 것임을 증명하는 것을 의미합니다. 문제는 항상 실제 로봇은 연속적인 세계에서 움직이는 반면, 이러한 수학적 증명은 세상을 고정된 단계의 격자로 나누어야 한다는 점이었습니다. 단계가 너무 크면 증명이 작은 사고를 놓치게 되고, 단계가 너무 작으면 컴퓨터가 방대한 가능성의 수에 압도되어 계산을 끝내지 못하게 됩니다.

스웨덴의 멜라르달렌 대학교(Mälardalen University)와 KTH 왕립 공과대학교(KTH Royal Institute of Technology)의 연구진은 이 간극을 메울 새로운 방법을 개발했습니다. 그들은 엔지니어가 'Timed Rebeca'라는 특화된 모델링 언어를 사용하여 다중 로봇 팀을 설계할 수 있는 시스템을 만들었는데, 이 언어는 각 로봇을 메시지에 반응하는 독립적인 행위자로 취급합니다. 이 모델은 이후 안전성을 보장하기 위해 컴퓨터에 의해 엄격하게 검사됩니다. 결정적으로, 연구팀은 로봇을 위한 실제 소프트웨어를 'ROS2'라는 표준 시스템을 사용하여 작성함으로써 수학적 모델과 실제 코드가 완벽하게 일치하도록 했습니다. 그들은 단순히 로봇을 시뮬레이션한 것이 아니라, 컴퓨터가 검증할 수 있을 만큼 추상적이면서도 기계의 실제 물리 법칙을 반영할 수 있을 만큼 상세한 버전의 모델을 구축했습니다. 이를 통해 그들은 일반적인 시뮬레이션이 놓치기 쉬운 드물고 위험한 실패를 예측할 수 있었습니다.

연구진은 5대의 로봇이 50x50 격자(대형 창고 바닥 크기 정도)를 가로질러 이동하는 시나리오에 집중했습니다. 그들은 로봇들이 장애물을 피해 항해하고 목표 지점에 도달하기 위해 서로의 경로를 가로질러야 하는 복잡한 환경을 설정했습니다. 실제 세계에서 이 로봇들은 레이저 스캐너를 사용하여 물체를 감지하며, 초당 수백 번 측정을 수행합니다. 연구팀은 이러한 연속적인 레이저 빔과 부드러운 움직임을 컴퓨터가 논리를 확인할 수 있는 이산적인 단계로 어떻게 변환할지 고민해야 했습니다. 그들은 로봇의 속도와 주변을 스캔하는 빈도 사이에 엄격한 관계가 있음을 발견했습니다. 로봇이 너무 빠르게 움직이면, 센서가 경로상의 장애물을 인지하기도 전에 전체 거리를 지나쳐 버릴 수 있습니다. 연구진은 모델이 정확하려면 로봇의 속도가 센서 업데이트 시간보다 빠르게 격자 셀을 통과하지 못하도록 제한되어야 함을 증명했습니다. 신호 처리의 근본 원리에서 도출된 이 규칙은 디지털 모델이 잠재적인 충돌을 놓치지 않도록 보장했습니다.

컴퓨터 검증을 가능하게 하기 위해, 팀은 문제의 진실을 잃지 않으면서 세상을 단순화해야 했습니다. 그들은 로봇을 부드러운 형상이 아니라, 한 칸의 셀에서 다른 칸으로 이동하며 45도씩 회전하는 직사각형으로 표현했습니다. 그들은 로봇의 속도와 셀의 크기를 기준으로 셀 사이를 이동하는 데 걸리는 시간을 계산했습니다. 또한 사인(sine)이나 코사인(cosine)과 같은 복잡한 삼각함수 값을 미리 계산하여 룩업 테이블(lookup table)에 저장함으로써, 컴퓨터가 매번 처음부터 계산할 필요가 없도록 했습니다. 이러한 최적화를 통해 모델 체커는 수백만 개의 상태를 단 몇 분 만에 탐색할 수 있었습니다. 검사를 실행했을 때, 컴퓨터는 특정 규칙 세트가 충돌로 이어질지 아니-면 안전한 도착로 이어질지를 절대적인 확신을 가지고 알려줄 수 있었습니다.

실험 결과는 놀라웠습니다. 로봇들이 안전한 속도와 다양한 대기 시간을 갖도록 프로그래밍된 경우, 모델 체커는 5대의 로봇이 충돌하거나 갇히지 않고 목적지에 도달할 것임을 확인했습니다. 연구진이 실제 ROS2 코드를 시뮬레이션에서 실행했을 때도 로봇들은 모델이 예측한 대로 정확히 행동하며 혼잡한 공간을 성공적으로 통과했습니다. 그러나 위험한 상황을 만들기 위해 파라미터를 변경했을 때(예를 들어, 모든 로봇이 정확히 같은 속도로 움직이게 하거나 스캔율을 속도에 비해 너무 낮게 설정했을 때), 모델 체커는 즉시 결함을 찾아냈습니다. 모델은 충돌을 일으킬 수 있는 특정 사건의 순서를 식별했습니다. 실제 코드를 동일한 위험한 설정으로 실행했을 때, 시뮬레이션은 모델이 예측한 것과 똑같은 방식으로 충돌했습니다. 한 테스트에서는 모델이 불과 몇 천 개의 상태만을 탐색하고도 충돌을 찾아낸 반면, 실제 시뮬레이션은 5번 중 3번의 실패를 기록하며 그 위험이 실재하며 예측 가능하다는 것을 입증했습니다.

이 연구는 타이밍의 중요성도 강조했습니다. 한 시나리오에서 연구진은 로봇의 속도를 센서 업데이트율에 비해 간신히 빠를 정도로 설정했습니다. 모델 체커는 이 작은 안전 규칙 위반이 로봇들이 서로를 피하도록 프로그래밍되어 있더라도 충돌을 거의 불가피하게 만든다는 것을 찾아냈습니다. 컴퓨터는 로봇들이 교차점에 동시에 도착할 것이며, 서로를 제때 보지 못해 충돌할 것이라고 보여주었습니다. 실제 시뮬레이션에서도 로봇들이 서로를 피하는 데 실패하는 모습이 나타나 이를 확인해주었습니다. 이는 모델이 단순한 이론적 연습이 아니라, 인간 엔지니어가 간과할 수 있는 미묘하고 위험한 오류를 잡아낼 수 있는 실용적인 도구임을 입증했습니다.

연구진은 자신들의 접근 방식에도 한계가 있음을 인정했습니다. 현재 방식은 엔지니어가 수학적 모델과 실제 코드를 모두 수동으로 구축해야 하며, 이는 시간이 많이 걸리고 인적 오류를 유발할 수 있는 과정입니다. 또한, 현재 시스템은 5대의 로봇과 50x50 격자는 처리할 수 있지만, 100대의 로봇이나 훨씬 더 큰 지도로 확장하면 컴퓨터의 메모리를 빠르게 초과하게 된다는 점도 언급했습니다. 병목 현상은 로봇이 갈 수 있는 가능한 경로의 수에서 발생합니다. 로봇의 수와 지도의 크기가 증가함에 따라 조합의 수가 너무 빠르게 늘어나 컴퓨터가 이를 저장할 공간이 부족해지기 때문입니다. 그럼에도 불구하고, 이 연구는 복잡한 로보틱 시스템의 '디지털 트윈'을 충분히 단순하면서도 신뢰할 수 있을 만큼 정확하게 만드는 것이 가능하다는 것을 증명했습니다.

이 연구는 안전한 자율 시스템을 개발하는 새로운 길을 제시합니다. 로봇 소프트웨어 설계를 먼저 수학적 모델을 구축하고 검증하는 과정으로 다룸으로써, 엔지니어들은 단 한 대의 로봇을 제작하거나 배치하기 전에 치명적인 결함을 식별할 수 있습니다. 연구팀은 모델의 상세 수준과 계산 효율성 사이의 균ax를 정교하게 조절함으로써, 다중 로봇 시스템이 실제 세계에서 안전하게 작동할 것임을 검증할 수 있음을 보여주었습니다. 그들의 작업은 미래의 로봇 공학이 단순히 더 똑똑한 기계를 만드는 것이 아니라, 가장 중요한 순간에 그 기계들이 실패하지 않을 것임을 증명하는 더 나은 방법을 구축하는 데 달려 있음을 시사합니다.