로봇이 새로운 탐험가가 되어 인간에게 너무 위험한 작업인 핵폐기물 현장, 심우주, 그리고 해저를 탐사하는 세상을 상상해 보십시오. 하지만 여기에는 함정이 있습니다. 이 로봇들은 단순한 원격 제어 자동차가 아니라, 거대한 레고 세트처럼 만들어진 복잡하고 모듈화된 기계라는 점입니다. 이들은 센서(보는 기능), 브레인(생각하는 기능), 바퀴(움직이는 기능) 등 서로 소통하는 수많은 다양한 부품을 가지고 있습니다. 문제는, 백만 개의 레고 브릭을 조립했을 때 그 전체 탑이 무너지지 않을 것이라고 100% 확신하기가 매우 어렵다는 것입니다. 컴퓨터 과학의 세계에서 이것은 "검증(verification)"이라고 불리며, 이는 로보트가 당신이 원하는 대로 정확히 수행하고, 원치 않는 일은 절대 하지 않도록 증명하는 기술입니다. 이를 위해 과학자들은 종종 "계약(contracts)"을 사용합니다. 계약을 친구 사이의 약속이라고 생각해보십시오. "네가 깨끗한 방을 준다면(가정), 나는 너에게 샌드위치를 가져다줄 것을 약속해(보장)." 모두가 자신의 약속을 지킨다면, 전체 시스템은 제대로 작동합니다. 하지만 로봇이 복잡해지면, 모든 약속을 일일이 손으로 확인하는 것은 불가능합니다.

이 논문은 이러한 로봇의 약속을 확인하는 영리하고 새로운 방법을 소개하며, 특히 ROS(Robot Operating System)라는 인기 있는 툴킷을 사용하여 구축된 로봇에 초점을 맞춥니다. 저자들인 컴퓨터 과학자 팀은 "구성적(compositional)" 접근 방식을 제안합니다. 로봇 전체를 한꺼번에 검증하려고 시도하는 대신(이는 마치 눈을 가리고 거대한 퍼즐을 맞추려는 것과 같습니다), 로봇을 개별 부품, 즉 "노드(nodes)"로 나눕니다. 그들은 각 노드에 대해 특정 계약을 작성하여, 만약 노드가 올바른 입력을 받는다면 반드시 올바른 출력을 낼 것임을 증명합니다. 그런 다음, 이 개별 계약들을 서로 맞물리게 하는 특별한 논리 규칙(칼큘러스, calculus)을 사용하여, 만약 모든 조각이 자신의 약속을 지킨다면 전체 로봇이 최종적인 큰 약속을 지킬 것임을 보여줍니다. 그들은 심지어 작성된 계약을 실시간으로 로봇을 감시하며 약속이 깨지는 즉시 "정지!"라고 외칠 디지털 "보안 요원"으로 자동 변환하는 "Vanda"라는 도구도 구축했습니다.

이 아이디어를 테스트하기 위해, 팀은 단순히 코드를 작성한 것이 아니라 핵 저장 시설을 탐사하는 로봇 로버의 시뮬레이션을 구축했습니다. 로봇의 임무는 방사능을 확인하기 위해 12개의 서로 다른 지점을 방문하는 것이었습니다. 만약 방사능이 너무 높아지면, 로봇은 임무를 중단하고 출구로 돌아와야 했습니다. 팀은 로봇의 "두뇌"(에이전트), "눈"(방사능 센서), "다리"(내비게이션 시스템)에 대한 계약을 작성했습니다. 그런 다음 그들은 각 부분을 확인하기 위해 다양한 방법을 사용했습니다. 어떤 부분은 수학적 증명으로, 어떤 부분은 컴퓨터 시뮬레이션으로, 또 어떤 부분은 코드 리뷰로 확인되었습니다. 결과는 어떠했을까요? 시스템은 작동했습니다. 계약은 각기 다른 검증 방법들을 성공적으로 안내했고, 자동화된 "보안 요원"(런타임 모니터)은 로봇의 속도를 늦추지 않으면서도 로봇을 감시할 수 있었습니다. 이 논문은 이 방법이 서로 다른 사람이나 도구를 사용하여 만든 부품들로 구성된 복잡하고 모듈화된 로봇을 더 안전하고 신뢰할 수 있게 만드는 강력한 방법임을 시사합니다.

핵심 아이디어: 로봇 약속 이행 시스템

당신이 방사능이 있는 핵 폐기물 매립지를 탐사하는 거대하고 자율적인 로봇을 만들고 있다고 상상해 보십시오. 이 로봇은 하나의 금속 덩어리가 아닙니다. 이 로봇은 함께 협력하는 전문가 팀입니다. 한 부분은 A 지점에서 B 지점까지 가는 방법을 찾아내는 **내비게이터(Navigator)**입니다. 또 다른 부분은 공기 중의 방사능 수치를 측정하는 **센서(Sensor)**입니다. 세 번째는 센서가 본 것에 따라 다음에 어디로 갈지 결정하는 **브레인(Brain)**입니다.

예전에는 로봇이 벽에 부딪히거나 방사능에 타버리지 않도록 만들고 싶다면, 전체 로봇을 한꺼번에 테스트하려 했을 것입니다. 하지만 그것은 망치로 자동차 전체를 때려서 고장 난 엔진을 고치려는 것과 같습니다. 매우 지저분한 방식이며, 만약 문제가 발생하더라도 어떤 부분이 원인인지 알 수 없습니다.

이 논문은 더 똑똑한 방법인 **계약 시스템(The Contract System)**을 제로합니다.

각 로봇 부품을 공장의 노동자라고 생각해보십시오. 업무를 시작하기 전, 그들은 계약을 체결합니다.

• 가정 (The "If"): "당신이 깨끗한 데이터를 준다면, 나는 내 직무를 수행할 것을 약속합니다."
• 보장 (The "Then"): "당신이 깨끗한 데이터를 준다면, 나는 정확한 지도를 제공할 것을 약속합니다."

논문의 저자들은 컴퓨터가 이해할 수 있는 방식으로 이러한 약속을 기록하기 위해 RCL(ROS Contract Language)이라는 특별한 언어를 만들었습니다. 그들은 **1차 논리(First-Order Logic, FOL)**라는 유형의 수학을 사용하는데, 이는 "방사능이 빨간색이면 로봇은 반드시 멈춰야 한다"와 같은 문장을 매우 정밀하게 쓰는 방법입니다.

마법의 접착제: 칼큘러스(The Calculus)

여기서 까다로운 점이 있습니다. 내비게이터가 약속을 지키고 센서가 약속을 지킨다고 해서, 로봇 전체가 자동으로 작동한다는 보장은 없습니다. 내비게이터의 "출력"(지도)이 센서의 "입력"(필요한 데이터)과 실제로 일치하는지 알아야 합니다.

저자들은 접착제 역할을 할 **칼큘러스(Calculus, 논리 규칙 집합)**를 구축했습니다. 이것은 마치 마스터 퍼즐 해결사와 같습니다.

1. 내비게이터의 계약을 입력합니다.
2. 센서의 계약을 입력합니다.
3. 칼큘러스는 다음과 같이 확인합니다: "내비게이터가 지도를 줄 것이라는 약속이 센서가 지도를 받을 것이라는 약속과 일치하는가?"
4. 만약 일치한다면, 칼큘러스는 이들을 결합하여 시스템 수준의 약속을 만듭니다: "로봇이 배터리를 가지고 시작한다면, 결국 모든 안전한 지점을 방문할 것이다."

이것을 **구성적 검증(Compositional Verification)**이라고 합니다. 즉, 작은 조각들을 따로 검증한 다음, 그 조각들이 어떻게 맞물리는지만 확인하여 전체가 작동함을 증명할 수 있다는 뜻입니다.

안전망: Vanda와 보안 요원

계약을 작성하는 것도 좋지만, 로봇이 실제로 작동하는 동안 혼란에 빠지면 어떻게 될까요? 센서에 오류가 생기면 어떡하죠?

저자들은 Vanda라는 도구를 만들었습니다. Vanda는 번역기와 보안 요원의 역할을 동시에 수행합니다.

1. 번역기: 작성된 계약(RCL)을 받아 로봇에서 실행될 수 있는 코드로 변환합니다.
2. 보안 요원 (런타임 모니터): 로봇이 작동하는 동안, Vanda는 로봇이 주고받는 모든 메시지를 감시하는 작은 "보안 요원"을 생성합니다. 만약 내비게이터가 "나는 문 앞에 있다"라고 말했는데, 계약상 "방사능이 낮을 때만 문 앞에 있을 수 있다"라고 되어 있다면, 보안 요원은 방사능을 확인합니다. 만약 방사능이 높다면, 보안 요원은 "위반!"이라고 외칩니다.

논문은 이 보안 요원들이 매우 효율적임을 보여줍니다. 테스트에서 이 보안 요원들을 추가해도 로봇의 속도가 거의 느려지지 않았습니다. 이는 자동차에 보안 카메라를 설치하는 것과 같습니다. 자동차는 여전히 빠르게 달릴 수 있지만, 이제 누군가 물건을 훔치려 하는지 알 수 있게 된 것입니다.

테스트 드라이브: 핵 폐기물 로버

이 방법이 효과적임을 증명하기 위해, 팀은 단순히 말로만 설명하지 않고 핵 폐기물 저장소를 탐사하는 Jackal 로버(Clearpath Robotics에서 제작한 실제 로봇)의 시뮬레이션을 구축했습니다.

• 임무: 로봇은 방사능 수치를 확인하기 위해 12개의 특정 지점(웨이포인트)을 방문해야 했습니다.
• 규칙:
  • 방사능이 낮으면(초록색) 또는 중간이면(주황색), 계속 진행합니다.
  • 방사능이 높으면(빨간색), 즉시 멈추고 출구로 돌아와야 합니다.
  • 모든 지점은 적어도 한 번씩 방문해야 합니다.

그들은 이 로봇에 자신들의 방법을 적용했습니다:

1. 1단계: 로봇의 소프트웨어를 살펴보고 이를 네 가지 주요 부분인 에이전트(두뇌), 내비게이션(다리), 방사능 센서(눈), 로컬라이제이션(방향 감각)으로 단순화했습니다.
2. 2단계: 각 부분에 대한 계약을 작성했습니다. 예를 들어, 에이전트의 계약은 "방사능이 빨간색인 것을 보면, 나는 로봇에게 출구로 이동하라는 명령을 내릴 것이다"라고 명시했습니다.
3. 3단계: 칼큘러스를 사용하여, 센서가 빨간색을 감지하면 에이전트가 이동 명령을 내리고, 내비게이션이 실제로 로봇을 움직일 것임을 증명했습니다.
4. 4단계: 각 부분을 서로 다른 방식으로 검증했습니다.
   • 에이전트(두뇌)는 모델 체커(프로그램이 갈 수 있는 모든 경로를 테스트하는 도구)를 통해 확인되었습니다.
   • 내비게이션(다리)은 로봇이 무작위 지점으로 이동하도록 하는 47번의 시뮬레이션을 통해 테스트되었습니다. 평균적으로 목표 지점에서 21.4cm 오차 내로 도착하여 허용된 안전 범위를 충족했습니다.
   • 방사능 센서는 방사능을 초록, 주황, 빨강으로 올바르게 분류하는지 확인하기 위해 수학적 증명(Hoare Logic)으로 확인되었습니다.
5. 5단계: Vanda 모니터를 켰습니다. 로봇은 임무를 수행했고, 모니터는 밀착 감시했습니다. 모니터는 로봇이 규칙을 준수했음을 확인했습니다: 즉, 지점들을 방문했고 방사능이 높아지자 즉시 탈출했습니다.

이것이 미래에 의미하는 바

이 논문은 이 접근 방식이 특히 여러 부품으로 만들어진 복잡한 로봇을 구축하는 데 있어 게임 체인저가 될 것임을 시사합니다.

• 믹스 앤 매치 (Mix and Match): 모든 사람이 계약에 동의하기 때문에, "두뇌"를 다른 것으로 교체할 수 있습니다. 어떤 팀은 화려한 AI를 사용하고, 다른 팀은 단순한 코드를 사용할 수도 있습니다. 두 팀 모두 동일한 계약(동일한 일을 하겠다는 약속)에 서명하기만 하면, 칼큘러스는 로봇이 여전히 작동할 것임을 보장합니다.
• 이질적 검증 (Heterogeneous Verification): 모든 부분을 동일한 도구로 확인할 필요가 없습니다. 어떤 부분은 수학으로, 어떤 부분은 시뮬레이션으로, 또 어떤 부분은 테스트로 확인하는 것이 가장 좋습니다. 계약은 이 모든 서로 다른 방법들을 하나로 묶어주는 공통 언어 역할을 합니다.
• 실시간 안전성 (Real-Time Safety): 런타임 모니터는 최종 안전망 역할을 합니다. 검증 단계에서 무언가를 놓쳤더라도, 모니터가 로봇이 실제로 작동하는 동안 위험한 행동을 하는지 포착할 것입니다.

저자들은 이 방법이 아직 완벽하지 않다는 점을 인정합니다. 이 방식은 데이터가 순차적으로 흐른다고 가정하며, 현재 "접착제"(칼큘러스)를 적용하는 과정은 컴퓨터가 아닌 사람이 수행합니다. 하지만 그들은 시뮬레이션에서 이 방법이 작동함을 보여주었으며, 이를 더욱 발전시킬 명확한 경로를 제시했습니다.

요약하자면, 이 논문은 우리의 로봇 조력자들에 대한 신뢰를 구축하는 새로운 방법을 제시합니다. 로봇이 잘 작동하기를 막연히 바라는 대신, 우리는 그들의 약속을 글로 적고, 그 약속들이 서로 잘 맞는지 확인하며, 그들이 약속을 지키는지 감시하는 보안 요원을 배치할 수 있습니다. 로봇이 언젠가 핵 폐기물을 청소하거나 화성을 탐사하게 될 세상에서, 이러한 안심은 무엇과도 바꿀 수 없는 가치입니다.