396.77 런타임 검증(Runtime Verification) 기법

1. 개요

런타임 검증(Runtime Verification, RV)은 시스템의 실행 흐름을 실시간으로 관찰(observe)하여, 사전에 정의된 형식 명세(formal specification)의 준수 여부를 판정하는 경량 형식 기법(lightweight formal method)이다. 전통적 모델 검사(model checking)가 설계 시점에서 시스템의 모든 가능한 상태를 탐색하는 반면, 런타임 검증은 실제 실행 경로(concrete execution trace)만을 대상으로 하므로 상태 폭발 문제를 회피할 수 있다. 로봇 임무 관리에서 런타임 검증은 임무 실행 중 안전 속성 위반, 제약 조건 침범, 비정상 행동을 즉각적으로 탐지하여 적시에 교정 조치를 개시하는 핵심 메커니즘으로 기능한다. 본 절에서는 런타임 검증의 이론적 기초, 모니터 구성 기법, 시간 명세 언어, 그리고 로봇 임무 관리에의 적용을 체계적으로 다룬다.

2. 런타임 검증의 기본 원리

2.1 런타임 검증의 정의

런타임 검증은 Leucker & Schallhart(2009)에 의해 다음과 같이 정의된다. 시스템 \mathcal{S}의 실행이 생성하는 이벤트 시퀀스(event sequence) \sigma = e_0 \, e_1 \, e_2 \, \ldots에 대해, 형식 명세 \varphi의 만족 여부를 판정하는 모니터(monitor) \mathcal{M}_\varphi를 구성하고, 이를 시스템에 부착하여 실시간으로 평가하는 기법이다.

\mathcal{M}_\varphi : \Sigma^* \rightarrow \{ \top, \bot, \; ? \}

여기서 \Sigma^*는 이벤트 시퀀스의 집합이며, 모니터의 출력은 다음을 의미한다.

• \top (참): 현재까지의 실행이 명세를 확정적으로 만족한다.
• \bot (거짓): 현재까지의 실행이 명세를 확정적으로 위반한다.
• ? (미결정): 현재까지의 실행으로는 판정할 수 없으며, 추가 이벤트를 관찰해야 한다.

2.2 오프라인 검증과 온라인 검증

런타임 검증은 모니터링 시점에 따라 두 가지로 구분된다.

로봇 임무 관리에서는 온라인 검증이 핵심적이다. 임무 실행 중 안전 위반이 발생하면 즉시 탐지하여 비상 프로토콜을 개시해야 하기 때문이다.

2.3 모니터의 판정 의미론

유한 트레이스(finite trace)에 대한 런타임 검증의 판정 의미론은 전통적 LTL(무한 트레이스 기반)과 상이하다. Bauer et al.(2011)은 다음의 3값 의미론(three-valued semantics)을 제안하였다.

[\sigma \models \varphi]_3 = \begin{cases} \top & \text{if } \forall \sigma' \in \Sigma^\omega: \sigma \cdot \sigma' \models \varphi \\ \bot & \text{if } \forall \sigma' \in \Sigma^\omega: \sigma \cdot \sigma' \not\models \varphi \\ ? & \text{otherwise} \end{cases}

이 의미론에서 \sigma는 현재까지 관찰된 유한 트레이스이며, \sigma \cdot \sigma'는 \sigma에 임의의 무한 연장 \sigma'를 접합한 것이다. 모니터는 현재 관찰한 유한 트레이스만으로는 최종 판정을 내릴 수 없는 경우 ?를 반환한다.

3. 명세 언어

3.1 LTL(Linear Temporal Logic) 기반 명세

LTL은 런타임 검증에서 가장 널리 사용되는 명세 언어이다. 로봇 임무 관리에서의 대표적 LTL 명세 예시는 다음과 같다.

안전 속성: 금지 구역 미진입

\square \neg \text{in\_forbidden\_zone}

순서 속성: 이륙 전 체크리스트 완료

\neg \text{takeoff} \; \mathcal{U} \; \text{checklist\_done}

응답 속성: 장애물 감지 후 일정 시간 내 회피 기동

\square \left( \text{obstacle\_detected} \rightarrow \Diamond_{[0, \tau]} \text{avoidance\_executed} \right)

3.2 STL(Signal Temporal Logic)

신호 시간 논리(Signal Temporal Logic, STL)(Maler & Nickovic, 2004)는 실수값 신호(real-valued signal)에 대한 시간적 속성을 표현하며, 로봇의 연속 값 센서 데이터를 직접 다루는 데 적합하다.

STL의 기본 술어는 실수값 함수의 부등식이다.

\mu := f(s(t)) > 0

여기서 s(t)는 시간 t에서의 신호값, f는 실수값 함수이다. STL의 시간 연산자는 LTL과 유사하되, 실수 시간 구간이 부가된다.

\varphi ::= \mu \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \varphi_1 \mathcal{U}_{[a,b]} \varphi_2

STL의 특장점은 정량적 의미론(quantitative semantics)을 제공하는 것이다. 로버스트니스 도(robustness degree) \rho(\varphi, s, t)는 명세 만족의 정도를 실수값으로 나타낸다.

\rho(\mu, s, t) = f(s(t))

\rho(\neg \varphi, s, t) = -\rho(\varphi, s, t)

\rho(\varphi_1 \wedge \varphi_2, s, t) = \min\left(\rho(\varphi_1, s, t), \; \rho(\varphi_2, s, t)\right)

\rho(\Diamond_{[a,b]} \varphi, s, t) = \sup_{t' \in [t+a, t+b]} \rho(\varphi, s, t')

\rho(\square_{[a,b]} \varphi, s, t) = \inf_{t' \in [t+a, t+b]} \rho(\varphi, s, t')

\rho > 0이면 명세를 만족하고, \rho < 0이면 위반한다. \vert\rho\vert의 크기는 만족/위반의 여유 정도를 나타내므로, 임무 관리에서 위반 임박 경고(pre-violation alert)를 발생시키는 데 활용된다.

3.3 MTL(Metric Temporal Logic)

메트릭 시간 논리(Metric Temporal Logic, MTL)(Koymans, 1990)는 LTL에 정량적 시간 제약을 추가한 논리로, 시간 한정(time-bounded) 속성의 표현에 적합하다.

\square_{[0, T]} \left( \text{battery\_level} > \text{threshold} \right): \text{시간 } T \text{까지 배터리 수준이 임계값 이상}

4. 모니터 구성 기법

4.1 오토마타 기반 모니터

LTL 명세로부터 모니터를 자동 구성하는 표준적 방법은 오토마타 이론에 기반한다.

1. LTL 명세 \varphi를 부정 정규형(Negation Normal Form)으로 변환한다.
2. **비결정적 뷔히 오토마톤(Nondeterministic Büchi Automaton, NBA)**을 구성한다.
3. **결정적 모니터 오토마톤(Deterministic Monitor Automaton)**으로 변환한다.

모니터 오토마톤 \mathcal{A}_\varphi = (Q, \Sigma, \delta, q_0, F_\top, F_\bot)에서 Q는 상태 집합, \Sigma는 입력 알파벳(이벤트 집합), \delta: Q \times \Sigma \rightarrow Q는 전이 함수, q_0는 초기 상태, F_\top은 확정적 만족 상태 집합, F_\bot은 확정적 위반 상태 집합이다.

모니터의 실행 시간 복잡도는 O(|\sigma|)로, 이벤트 시퀀스의 길이에 선형적이다. 공간 복잡도는 모니터 오토마톤의 상태 수 |Q|에 의존하며, LTL 명세의 크기에 대해 최악의 경우 지수적(2^{O(|\varphi|)})이나, 실용적 임무 명세에서는 관리 가능한 수준이다.

4.2 표 기반 모니터(Table-Based Monitor)

실시간 성능이 중요한 로봇 시스템에서는 오토마톤 전이 테이블을 사전 계산하여 룩업 테이블(look-up table)로 구현한다. 이를 통해 각 이벤트 수신 시 O(1)의 시간으로 상태를 전이시킬 수 있다.

4.3 재작성 기반 모니터(Rewriting-Based Monitor)

명세 수식을 현재 이벤트에 기반하여 점진적으로 재작성(rewrite)하는 방식이다. 이벤트 e를 관찰한 후, 잔여 명세(residual specification)를 다음과 같이 갱신한다.

\varphi' = \text{progress}(\varphi, e)

이 방법은 명세의 구조를 유지하므로 디버깅과 진단에 용이하다.

5. 로봇 임무 관리에의 적용

5.1 모니터 삽입 아키텍처

런타임 모니터를 로봇 임무 관리 시스템에 삽입하는 방법은 다음의 세 가지 패턴으로 분류된다.

인라인 모니터(Inline Monitor): 임무 관리 코드 내부에 모니터 로직을 직접 삽입한다. 오버헤드가 최소이나, 모니터와 시스템 코드 간의 결합도(coupling)가 높아 유지보수가 어렵다.

사이드 모니터(Side Monitor): 임무 관리 시스템과 독립된 프로세스로 모니터를 실행하고, 이벤트 버스(event bus)를 통해 관찰 데이터를 수신한다. 모듈성이 높으나, 프로세스 간 통신에 의한 지연이 발생한다.

하이브리드 모니터(Hybrid Monitor): 안전 필수 속성은 인라인으로, 성능 관련 속성은 사이드 모니터로 감시하는 혼합 구조이다.

5.2 ROS2 기반 런타임 검증 통합

ROS2(Robot Operating System 2) 환경에서 런타임 검증을 통합하는 대표적 방법은 다음과 같다.

1. 토픽 구독 기반 모니터: ROS2 토픽(topic)을 구독하여 센서 데이터, 임무 상태, 제어 명령 등의 이벤트 스트림을 수신하고, 모니터가 실시간으로 명세를 평가한다.

2. 라이프사이클 노드 연동: ROS2 Lifecycle 노드의 상태 전이 이벤트를 모니터하여, 임무 관리 노드의 비정상 전이를 탐지한다.

3. DDS QoS 기반 감시: DDS(Data Distribution Service)의 QoS(Quality of Service) 메트릭(지연, 손실률 등)을 모니터하여 통신 품질 저하에 의한 임무 위험을 선제적으로 탐지한다.

5.3 적응적 대응(Reactive Adaptation)

런타임 검증 결과에 기반한 적응적 대응 메커니즘은 다음의 단계로 구성된다.

1. 위반 탐지(Violation Detection): 모니터가 명세 위반(\bot) 또는 위반 임박(\rho < \epsilon)을 탐지한다.

2. 심각도 분류(Severity Classification): 위반의 심각도를 분류한다.

3. 교정 행동 실행(Corrective Action Execution): 임무 재계획, 안전 모드 전환, 비상 착륙 등의 교정 행동을 실행한다.

6. 성능 고려 사항

6.1 모니터링 오버헤드

런타임 검증 모니터의 실행은 로봇 시스템의 연산 자원을 소비하므로, 오버헤드를 최소화하는 것이 중요하다. 오버헤드의 원천과 완화 전략은 다음과 같다.

6.2 이벤트 샘플링

모든 이벤트를 모니터하는 것이 비용 면에서 비현실적인 경우, 확률적 샘플링을 적용한다. 샘플링 비율 p_s에서의 위반 탐지 확률은 다음과 같다.

P(\text{detect}) = 1 - (1 - p_s)^{n_v}

여기서 n_v는 위반 이벤트의 수이다. 안전 필수 속성에 대해서는 p_s = 1(전수 모니터링)을 적용하고, 비안전 속성에 대해서는 적절한 샘플링 비율을 설정한다.

7. 주요 도구와 프레임워크

런타임 검증에 활용되는 대표적 도구와 프레임워크는 다음과 같다.

8. 한계와 도전 과제

런타임 검증 기법의 주요 한계와 도전 과제는 다음과 같다.

1. 관찰 불완전성: 모니터가 시스템의 모든 내부 상태를 관찰할 수 없는 경우, 명세의 판정 능력이 제한된다. 관찰 가능한 이벤트만으로 충분한 검증이 가능한 명세를 설계하는 것이 과제이다.

2. 모니터 자체의 신뢰성: 모니터 소프트웨어의 오류가 오탐(false positive) 또는 미탐(false negative)을 유발할 수 있다. 모니터의 형식적 정확성(correctness) 증명이 필요하다.

3. 다중 로봇 시스템의 분산 모니터링: 다수의 로봇이 협력하는 분산 임무에서는 전역 속성의 모니터링을 위해 분산 모니터 간의 동기화가 필요하며, 이는 통신 지연과 일관성 문제를 야기한다.

4. 연속 시간 시스템의 모니터링: 로봇의 물리적 동작은 연속 시간계로 기술되나, 디지털 모니터는 이산 샘플에 기반하므로, 샘플링 주기와 명세 의미론 간의 정합성을 보장해야 한다.

5. 학습 기반 구성요소와의 통합: 신경망 기반 인식 모듈의 출력에 대한 런타임 검증은, 출력의 확률적 특성과 블랙박스 성격으로 인해 명세 작성과 모니터 설계에 추가적 난이도가 존재한다.

9. 참고 문헌

• Leucker, M., & Schallhart, C. (2009). “A Brief Account of Runtime Verification.” Journal of Logic and Algebraic Programming, 78(5), 293–303.
• Bauer, A., Leucker, M., & Schallhart, C. (2011). “Runtime Verification for LTL and TLTL.” ACM Transactions on Software Engineering and Methodology, 20(4), 1–64.
• Maler, O., & Nickovic, D. (2004). “Monitoring Temporal Properties of Continuous Signals.” Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Springer.
• Koymans, R. (1990). “Specifying Real-Time Properties with Metric Temporal Logic.” Real-Time Systems, 2(4), 255–299.
• Donzé, A. (2010). “Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems.” Computer Aided Verification, Springer.
• Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A., & Rosu, G. (2014). “ROSRV: Runtime Verification for Robots.” Runtime Verification, Springer.
• Reinbacher, T., Rozier, K. Y., & Schumann, J. (2014). “Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems.” International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

본 절은 로봇공학 서적 시리즈의 일부로서 버전 1.0(2026년 3월)에 해당한다.