💻 computer science

Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification

이 논문은 기존의 설계 시점 모델을 활용하여 자율 시스템의 안전 위반을 더 조기에 탐지할 수 있도록 CSP 기반의 적합성 모니터링과 예측적 LTL 분석을 결합한 2단계 런타임 검증 파이프라인인 Predictive Varanus를 소개한다.

원저자: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

게시일 2026-09-17

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

화성을 탐사하는 로버부터 택배를 배달하는 드론에 이르기까지, 자율 주행 로봇들은 결코 완전히 예측할 수 없는 세상 속에서 작동합니다. 가장 정교하게 설계된 기계라 할지라도 센서 오류, 예상치 못한 장애물, 또는 엔지니어가 상상하지 못한 상황에 직면할 수 있습니다. 이러한 시스템을 안전하게 유지하기 위해 과학자들은 '런타임 검증(runtime verification)'이라는 기술을 사용합니다. 이것은 마치 로봇의 모든 움직임을 실시간으로 지켜보며, 미션 시작 전에 작성된 일련의 규칙에 따라 로봇의 행동을 점검하는 빈틈없는 부조종사와 같습니다. 만약 로봇이 금지된 행동을 하려 한다면, 부조종사는 경보를 울립니다. 그러나 이 전통적인 방식에는 결정적인 결함이 있습니다. 바로 사후 반응적(reactive)이라는 점입니다. 이는 나쁜 사건이 이미 발생한 후에야 경보를 울린다는 것을 의미합니다. 원자력 시설이나 심우주 미션과 같이 이해관계가 걸린 고위험 환경에서는, 실수가 발생한 후에 반응하는 것은 너무 늦을 수 있습니다. 연구자들의 목표는 단순히 오류를 감시하는 것이 아니라, 로봇이 첫 발을 내딛기도 전에 실패를 예측하여 오류를 예견하는 시스템을 구축하는 것입니다.

이것이 바로 '프리딕티브 바라누스(Predictive Varanus)'라는 새로운 모니터링 시스템을 개발한 연구팀이 해결하고자 하는 과제입니다. 이 시스템은 자율 주행 로봇을 위해 설계되었으며, 핵폐기물 저장소를 점검하는 임무를 맡은 시뮬레이션 로버를 대상으로 테스트되었습니다. 연구진은 두 가지 기존 기술을 결러 합쳐, 로봇이 해야 할 행동에 대해서는 엄격하면서도 다음에 일어날 일을 내다볼 만큼 똑똑한 파이프라인을 만들었습니다. 시스템의 첫 번째 부분은 문지기 역할을 합니다. 이 부분은 '통신 순차 프로세스(Communicating Sequential Processes)'라고 불리는 형식 언어로 작성된 로봇의 의도된 행동에 대한 상세한 지도를 사용하여, 로봇이 수행하는 모든 이벤트를 점검합니다. 만약 로봇이 방문해서는 안 될 위치로 이동하려고 하거나 안전 명령을 무시한다면, 문지기는 즉시 해당 동작을 유효하지 않은 것으로 거부합니다. 이는 로봇이 설계된 경계 내에 머물도록 보장합니다.

시스템의 두 번째 부분은 예측이 일어나는 곳입니다. 문지기가 로봇의 현재 행동이 유효함을 확인하면, 시스템은 앞을 내다봅니다. 시스템은 다음과 같은 단순하지만 강력한 질문을 던집니다. "로봇이 지금 올바르게 행동하고 있다면, 앞으로 가질 수 있는 가능한 미래는 오직 무엇인가?" 로봇의 설계 지도에 의해 허용된 남은 경로들을 분석함으로써, 시스템은 특정 결과가 이제 피할 수 없는 것인지 판단할 수 있습니다. 이 시스템은 무작위로 가능성을 추측하는 것이 아니라, 로봇의 규칙과 일치하는 미래만을 고려합니다. 만약 로봇이 높은 방사선 수치에 도달했다면, 시스템은 허용된 유일한 미래 경로가 돌아와서 미션을 중단하는 것임을 알게 됩니다. 따라서 로봇이 실제로 회항하기 전이라도, 시스템은 미션이 실패할 것임을 확실히 예측할 수 있습니다. 마찬가지로, 로봇이 필요한 모든 체크포인트를 성공적으로 방문했다면, 시스템은 로봇이 공식적으로 멈추기 전까지 몇 번의 움직임이 더 남아 있더라도 미션이 성공할 것이라고 예측할 수 있습니다.

연구진은 이 접근 방식을 다섯 개의 웨이포인트를 방문하고 방사선 수치를 확인하도록 프로그래밍된 핵 점검 로버에 테스트했습니다. 방사선 수치는 녹색, 주황색, 빨간색으로 분류되었습니다. 만약 로버가 주황색이나 빨간색을 감지하면, 규칙에 따라 출발지로 돌아와 미션을 중단해야 합니다. 표준 모니터링 방식에서는 로버가 실제로 돌아선 후에야 미션이 실패했음을 알게 됩니다. 하지만 프리딕티브 바라누스를 사용하면, 로버가 복귀 여정을 시작하기 두 이벤트 전부터 미션 실패를 선언할 수 있었습니다. 다른 시나리오에서는, 로봇이 마지막 과업을 완수하기 여덟 이벤트 전에도 성공적인 완료를 예측할 수 있었습니다. 이러한 조기 경보는 인간 운영자나 로봇 자체의 제어 소프트상이 단순히 실패가 펼쳐지는 것을 지켜보는 대신, 경로를 재설계하거나 안전한 종료를 준비하는 등 대응할 수 있는 귀중한 시간을 제공합니다.

또한 연구진은 이 추가적인 사고 계층이 얼마나 많은 컴퓨计算 능력을 요구하는지도 측정했습니다. 문지기 부분은 로봇의 행동 지도가 커지더라도 이벤트당 1밀리초 미만이 걸릴 정도로 매우 빨랐습니다. 앞을 내다보는 작업을 수행하는 예측 부분은 로봇의 가능한 행동이 더 복잡해짐에 따라 더 많은 시간이 걸렸습니다. 200개의 서로 다른 상태를 가진 모델의 경우, 예측 점검에는 이벤트당 약 700밀리초가 소요되었습니다. 비록 더 느리긴 하지만, 연구진은 결과를 미리 아는 데서 오는 이점이 많은 상황에서 그 비용을 감수할 가치가 있다는 것을 발견했습니다. 시스템은 로봇이 여전히 규칙을 따르고 있는 상황에서도 피할 수 없는 실패와 피할 수 없는 성공을 성공적으로 식별해 냈으며, 이는 현재의 법칙을 어기지 않고도 미래를 들여다보는 것이 가능하다는 것을 입증했습니다.

이 연구가 중요한 이유는 단순히 미래를 예측하기 때문이 아니라, 어떻게 예측하느냐에 있습니다. 이 시스템은 예측을 위해 별도의 추상적인 모델에 의존하지 않습니다. 대신, 로봇의 행동을 검증하는 데 사용했던 것과 정확히 동일한 설계 지도를 재사용합니다. 이는 시스템이 로봇이 어떻게 행동할지에 대해 가정하는 것이 아니라, 엔지니어가 이미 기계에 구축해 놓은 논리를 엄격히 따르고 있음을 의미합니다. 연구진은 현재의 유효성에 대한 엄격한 점검과 미래의 필연성에 대한 전방향 점검을 결합함으로써, 표준 모니터링보다 더 빠르고 유용한 판결을 제공할 수 있음을 보여주었습니다. 이 시스템은 무작위적인 실패나 센서 오류를 예측하는 것이 아니라, 모델링되지 않은 오류를 예측하는 것이 아니라, 로봇의 설계로부터 비롯된 논리적 결과를 예측합니다. 자율 주행 로보틱스의 복잡하고 불확리한 세상에서, 올바른 경로의 필연적인 결과를 바라보는 이 능력은 단순한 사후 반응형 경보를 선제적인 가이드로 바꾸며 새로운 종류의 안전을 제공합니다.

기술 요약: Predictive Varanus

문제 정의
런타임 검증(Runtime Verification, RV)은 자율 및 로봇 시스템을 위한 핵심 기술로, 소스 코드나 내부 상태에 대한 접근 없이 관찰된 실행 트레이스를 형식적 명세와 대조하여 온라인 보증을 제공한다. 그러나 표준 RV는 본질적으로 반응적(reactive)이다. 즉, 나쁜 이벤트가 이미 발생한 후에야 위반을 감지할 수 있다. 실패의 비용이 매우 큰 안전 필수 도메인에서 이러한 지연 시간은 불충분하다. 예측적 런타임 검증(Predictive Runtime Verification, PRV)은 가능한 미래의 연속(continuations)을 분석하여 속성의 필연적인 만족 또는 위반을 결정함으로써 이 문제를 해결하지만, 기존 방식은 종종 시스템의 설계 시점 명세와 구별되는 별도의 모델에 의존한다. 또한, 표준 PRV는 시스템이 모델에 따라 동작하면서 속성을 위반하는 경우와, 모델링되지 않은 방식(명세 외 동작)으로 동작하는 경우를 본질적으로 구분하지 못한다.

방법론
본 논문은 기존의 VARANUS 툴과 선형 시간 템포럴 로직(LTL)을 위한 예측적 런타임 검증을 통합한 2단계 검증 파이프라인인 PREDICTIVE VARANUS를 제시한다. 핵심 혁신은 단일한 설계 시점 Communicating Sequential Processes (CSP) 모델을 컨포먼스 체크(conformance checking)와 예측 추론 모두에 재사용하는 것이다.

파이프라인은 다음과 같이 작동한다:

CSP 컨포먼스 게이트 (VARANUS): 분석 대상 시스템(SUA)은 이벤트 트레이스를 방출한다. 첫 번째 단계에서는 CSP 모델을 결정론적 오라클(deterministic oracle)로 사용하여 VARANUS가 현재 트레이스가 CSP 모델의 언어의 유효한 접두사(prefix)인지 확인한다. 만약 이벤트가 모델에 의해 허용되지 않는다면, 트레이스는 즉시 거부(rej)된다. 이는 예측적 추론이 시스템의 설계와 일치하는 동작에 대해서만 적용되도록 보장한다.
모델 번역: 컨포먼스 게이트를 통과한 트레이스의 경우, CSP 모델은 Büchi 오토마타(Hanoi Omega-Automata 형식)로 번역된다. 이 번역 과정에는 다음이 포함된다:
- CSP 프로세스로부터 레이블된 전이 시스템(LTS) 추출.
- CSP 이벤트를 원자 명제(atomic propositions)로 매핑.
- 유한 트레이스를 무한 단어로 변환하여 표준 LTL 의미론을 가능하게 하기 위해 터미널 상태에 skip 셀프 루프 추가.
예측적 LTL 모니터링: 예측 모니터는 번역된 Büchi 오토마타를 사용하여 허용 가능한 미래의 집합을 제한한다. LTL 속성 $\phi$ $ϕ$ 가 주어지면, 모니터는 CSP 유래 오토마타와 $\phi$ $ϕ$ 및 $\neg\phi$ $\neg ϕ$ 에 대한 오토마타의 동기 곱(synchronous products)을 계산한다.
- 모든 모델 일치 연속이 $\phi$ 를 만족하면, 결론적인 만족( $\top$ ) 판정을 내린다.
- 모든 모델 일치 연속이 $\phi$ 를 위반하면, 결론적인 위반( $\bot$ ) 판정을 내린다.
- 두 결과가 모두 가능한 경우, 판정은 미결정( $?$ )이다.
- 트레이스가 VARANUS에 의해 거부된 경우, 판정은 rej이다.

주요 기여

통합 파이프라인: 본 논문은 CSP 기반 컨포먼스 모니터링과 예측적 LTL 검증을 결합한 공식적인 2단계 파이프라인을 정의한다.
모델 재사용: 설계 시점 분석(예: FDR 또는 RoboChart 활용)에 일반적으로 사용되는 단일 CSP 모델이 어떻게 런타임 오라클(컨포먼스용)과 예측을 위한 허용 가능한 미래의 소스라는 두 가지 목적을 모두 수행할 수 있는지 보여준다.
형식 의미론: 저자들은 결합된 판정 함수에 대한 공식적인 정의를 제공하여, rej(모델 비적합)와 예측적 $\bot$ (모델 내에서의 필연적 위반)을 구분한다.
구현 및 번역: 본 연구는 CSP 프로세스로부터 프로포지셔널 $\omega$ -오토마타를 구축하는 상세 과정을 설명하며, 이를 통해 구조적 제약을 유지하면서도 표준 LTL 툴(예: Spot)을 사용할 수 있게 한다.

결과
본 접근 방식은 원자력 저장소 점검을 위한 로봇 로버 케이스 스터디와 합성 스트레스 테스트를 통해 평가되었다.

로버 케이스 스터디: 시스템은 미션 완료, 커버리지, 중단(abort) 조건에 관한 속성을 모니터링했다.
- 위험한 방사선이 감지되는 시나리오에서, 시스템은 실제 트레이스에서 중단 이벤트가 발생하기 1~2 이벤트 더 일찍 미션 실패(완료/커버리지 위반)와 중단의 필연성을 예측했다.
- 정상적인 미션의 경우, 커버리지 속성이 미션 완료 이벤트 8개 전에 만족될 것으로 예측되었다.
- 유효하지 않은 트레이스(예: 위험 상황 중에도 계속 진행하는 경우)는 VARANUS에 의해 즉시 거부되었으며, 이 경우 예측 이득은 없었다. 이는 시스템이 모델 외 동작을 올바르게 처리함을 확인시켜 준다.
- 런타임 오버헤드는 로버의 경우 적절한 수준이었다(총 이벤트당 약 1.84 ms). CSP 체크는 0.19 ms, 예측 모니터는 1.64 ms가 소요되었다.
합성 스트레스 테스트:
- 확장성: CSP 컨포먼스 체크는 모델 크기가 증가하더라도 가벼운 수준(<1 ms/event)을 유지했다. 그러나 예측 모니터의 비용은 모델 크기에 따라 크게 확장되었다(10개 상태에서 약 0.2 ms/event $\rightarrow$ 200개 상태에서 약 700 ms/event). 이는 오토마타 구축 및 유지 관리가 주요 병목 지점임을 나타낸다.
- 예측 이득(Anticipation Gain): 결정적 꼬리(decision-tail) 벤치마크에서, 예측에 의한 이득(예측을 통해 절약된 이벤트 수)은 약속 지점(commitment point) 이후 강제된 꼬리 길이와 선형적으로 증가했다. 꼬리 길이가 20일 때, 시스템은 반응형 모니터보다 21 이벤트 더 일찍 판정을 제공했다.

의의 및 주장
본 논문은 PREDICTIVE VARANUS가 기존의 설계 시점 CSP 모델을 활용하여 런타임 검증에서 더 빠른 판정을 달성하는 실용적인 방법을 제공한다고 주장한다. 그 의의는 다음과 같다:

실패 모드의 차별화: "모델 외(out-of-model)" 동작(VARANUS에 의해 감지됨)과 "모델 내에서의 필연적 속성 위반"(PRV에 의해 감지됨)을 명확히 구분한다.
운용적 유용성: 케이스 스터디는 예측된 판정이 물리적으로 나타나기 전, 즉 미션 중단이나 실패를 식별함으로써 인간 운영자나 재계획(re-planning) 알고리즘에 유용할 만큼 충분히 빨리 생성될 수 있음을 입증한다.
모듈성: 파이프라인은 모듈화되어 있다. 현재 구현은 LTL을 사용하지만, CSP 컨포먼스 계층을 변경하지 않고도 다른 예측 추론 기법을 통합할 수 있는 구조를 갖는다.

저자들은 현재 구현이 대규모 모델에 대한 예측 컴포넌트의 확장성 문제를 겪고 있음을 인정하며, 향후 연구가 오토마타 백엔드 최적화나 심볼릭 표현 탐색에 집중될 수 있음을 시사한다. 또한, 이들이 일반적인 물리적 실패를 예측하는 문제를 해결한다고 주장하는 것이 아니라, 시스템 자체의 설계 모델에 의해 강제되는 결과를 예측하는 것임을 명시한다.

유사한 논문