396.78 형식 검증(Formal Verification)과 임무 안전성

1. 개요

형식 검증(Formal Verification)은 수학적 엄밀성에 기반하여 시스템이 주어진 명세를 만족하는지를 증명하는 체계적 방법론이다. 로봇 임무 관리에서 형식 검증은 임무 계획의 정확성(correctness)과 안전성(safety)을 설계 시점에서 보증하는 핵심 수단으로, 시뮬레이션이나 테스팅으로는 달성할 수 없는 완벽한 커버리지를 제공한다. 특히 안전 필수(safety-critical) 로봇 시스템—무인 항공기, 자율 주행 차량, 의료 로봇 등—에서 형식 검증은 인증(certification) 요구의 충족과 규제 준수를 위해 불가결한 기법이다. 본 절에서는 형식 검증의 이론적 기초, 모델 검사와 정리 증명의 적용, 임무 안전성 보증 체계, 그리고 하이브리드 시스템 검증의 실용적 전략을 다룬다.

2. 형식 검증의 이론적 기초

2.1 형식 검증의 범주

형식 검증은 “시스템이 명세를 만족하는가?“라는 질문에 수학적으로 확정적인 답을 제공하는 것을 목적으로 한다. 이를 형식적으로 표현하면 다음과 같다.

\mathcal{M} \models \varphi

여기서 \mathcal{M}은 시스템 모델, \varphi는 형식 명세, \models는 만족 관계(satisfaction relation)이다. 형식 검증의 주요 범주는 다음과 같다.

1. 모델 검사(Model Checking): 시스템의 유한 상태 모델에 대해 모든 가능한 실행 경로를 자동으로 탐색하여 명세 위반 여부를 판정한다.

2. 정리 증명(Theorem Proving): 공리(axiom)와 추론 규칙(inference rule)에 기반하여 시스템 속성을 연역적으로 증명한다.

3. 추상 해석(Abstract Interpretation): 시스템의 의미론(semantics)을 수학적으로 추상화하여 속성을 근사적으로 검증한다.

2.2 건전성과 완전성

형식 검증 기법의 품질은 건전성(soundness)과 완전성(completeness)으로 평가된다.

• 건전성(Soundness): 검증 기법이 “만족“이라고 판정하면 실제로 명세가 만족된다. 즉, 오탐(false positive)이 없다.

\text{검증 결과} = \top \implies \mathcal{M} \models \varphi

• 완전성(Completeness): 시스템이 실제로 명세를 만족하면 검증 기법이 “만족“이라고 판정한다. 즉, 미탐(false negative)이 없다.

\mathcal{M} \models \varphi \implies \text{검증 결과} = \top

모델 검사는 유한 상태 시스템에 대해 건전하고 완전하다. 정리 증명은 건전하나, 일반적으로 완전하지 않다(Gödel의 불완전성 정리에 의해).

3. 모델 검사의 임무 관리 적용

3.1 임무 모델 구성

임무 관리 시스템을 모델 검사로 검증하기 위해서는 시스템을 크립키 구조(Kripke structure) 또는 시간 오토마톤(timed automaton)으로 모델링해야 한다. 임무 관리의 주요 구성 요소에 대한 모델링 전략은 다음과 같다.

3.2 검증 속성의 명세

임무 안전성과 관련된 검증 속성은 시간 논리(temporal logic)로 명세한다. 대표적인 안전 관련 속성 패턴은 다음과 같다.

무결성(Integrity): 임무 데이터의 무결성이 보존된다.

\square \left( \text{mission\_data\_valid} \right)

상호 배제(Mutual Exclusion): 두 로봇이 동시에 동일 자원을 사용하지 않는다.

\square \neg \left( \text{robot}_1.\text{using\_resource} \wedge \text{robot}_2.\text{using\_resource} \right)

교착 상태 회피(Deadlock Freedom): 시스템이 교착 상태에 빠지지 않는다.

\square \left( \exists \text{ enabled transition} \right)

시간 한정 응답(Bounded Response): 비상 신호 발생 후 T 시간 단위 이내에 비상 프로토콜이 개시된다.

\square \left( \text{emergency\_signal} \rightarrow \Diamond_{\leq T} \text{emergency\_protocol\_active} \right)

불변성(Invariant): 특정 상태 조합이 절대 발생하지 않는다.

\square \neg \left( \text{motors\_on} \wedge \text{self\_test\_active} \right)

3.3 상태 폭발 완화 기법

복잡한 다중 로봇 임무 시스템의 모델 검사에서는 결합 상태 공간이 기하급수적으로 증가하는 상태 폭발(state explosion) 문제가 발생한다. 이를 완화하기 위한 기법은 다음과 같다.

기호적 모델 검사(Symbolic Model Checking): 상태 집합을 이진 결정 다이어그램(Binary Decision Diagram, BDD) 또는 부울 만족 가능성(SAT) 공식으로 표현하여, 상태를 개별적으로 열거하지 않고 집합 수준에서 연산한다.

부분 순서 축약(Partial Order Reduction, POR): 독립적인 전이(independent transitions)의 실행 순서가 검증 결과에 영향을 미치지 않을 때, 대표 순서만 탐색하여 상태 공간을 축소한다. 다중 로봇 시스템에서 독립적인 로봇의 행동 순서가 해당된다.

반사실적 추상화(Counterexample-Guided Abstraction Refinement, CEGAR): 초기에는 거친 추상 모델을 검사하고, 반례가 발견되면 추상화를 정제(refine)하는 반복 과정을 수행한다(Clarke et al., 2003).

조합적 축약(Compositional Reduction): 전체 시스템을 한번에 검사하지 않고, 각 구성 요소를 개별적으로 검증한 후 합성 결과의 속성을 추론한다. 가정-보장(Assume-Guarantee) 추론이 대표적이다.

\frac{\langle A \rangle \; M_1 \; \langle G_1 \rangle, \quad \langle G_1 \rangle \; M_2 \; \langle G_2 \rangle}{\langle A \rangle \; M_1 \parallel M_2 \; \langle G_2 \rangle}

여기서 \langle A \rangle는 가정(assumption), \langle G \rangle는 보장(guarantee), M_1 \parallel M_2는 병행 합성이다.

4. 정리 증명의 임무 관리 적용

4.1 정리 증명 도구의 특성

정리 증명 도구(Interactive Theorem Prover)는 사용자가 증명을 구성하는 과정을 컴퓨터가 검증하는 반자동적 체계이다. 주요 도구의 특성 비교는 다음과 같다.

4.2 임무 관리 속성의 증명 기법

정리 증명으로 임무 관리의 안전성을 검증하는 전형적 접근은 다음과 같다.

1. 시스템 모델의 형식화: 임무 관리 시스템의 상태, 전이, 제약을 정리 증명 도구 내에서 수학적으로 정의한다.

2. 불변성 증명(Invariant Proof): 시스템의 모든 도달 가능 상태에서 안전 속성이 성립함을 귀납법(induction)으로 증명한다.

\text{Base Case}: \quad I(s_0)

\text{Inductive Step}: \quad I(s) \wedge s \xrightarrow{a} s' \implies I(s')

여기서 I(s)는 불변 조건(invariant), s_0는 초기 상태, s \xrightarrow{a} s'는 행동 a에 의한 상태 전이이다.

3. 정제 증명(Refinement Proof): 추상 임무 모델이 만족하는 속성이 구체적 구현에서도 보존됨을 증명한다.

5. 하이브리드 시스템의 형식 검증

5.1 하이브리드 오토마톤 모델

로봇은 이산적 임무 상태 전이와 연속적 물리 동역학을 결합한 하이브리드 시스템(hybrid system)이다. 하이브리드 오토마톤(Hybrid Automaton)(Henzinger, 1996)은 이를 형식적으로 모델링하는 구조이다.

하이브리드 오토마톤 \mathcal{H} = (Q, X, \text{Init}, f, \text{Inv}, E, G, R)은 다음과 같이 정의된다.

• Q: 이산 상태(모드) 집합
• X \subseteq \mathbb{R}^n: 연속 상태 변수 공간
• \text{Init} \subseteq Q \times X: 초기 조건
• f: Q \times X \rightarrow \mathbb{R}^n: 각 모드에서의 연속 동역학 (\dot{x} = f(q, x))
• \text{Inv}: Q \rightarrow 2^X: 각 모드의 불변 조건(invariant)
• E \subseteq Q \times Q: 이산 전이 간선
• G: E \rightarrow 2^X: 전이 가드(guard) 조건
• R: E \times X \rightarrow 2^X: 전이 시 연속 상태 리셋 함수

5.2 도달 가능성 분석(Reachability Analysis)

하이브리드 시스템의 안전성 검증은 도달 가능 집합(reachable set) \mathcal{R}(t)을 계산하여 위험 영역 \mathcal{U}(unsafe set)과의 교집합이 공집합인지를 확인하는 것이 핵심이다.

\mathcal{R}(t) = \{ (q, x) \mid \exists (q_0, x_0) \in \text{Init}: (q_0, x_0) \xrightarrow{t} (q, x) \}

\text{Safe} \iff \forall t \geq 0: \mathcal{R}(t) \cap \mathcal{U} = \emptyset

도달 가능 집합의 정확한 계산은 일반적으로 불가능(undecidable)하므로, 과근사(over-approximation) 기법을 적용한다. 과근사 집합 \hat{\mathcal{R}}(t) \supseteq \mathcal{R}(t)에 대해 다음이 성립하면 안전성이 보장된다.

\hat{\mathcal{R}}(t) \cap \mathcal{U} = \emptyset \implies \mathcal{R}(t) \cap \mathcal{U} = \emptyset

대표적인 도달 가능 집합 과근사 도구는 다음과 같다.

5.3 제어 장벽 함수(Control Barrier Function)

제어 장벽 함수(Control Barrier Function, CBF)(Ames et al., 2017)는 안전 집합(safe set) \mathcal{C} = \{ x \in \mathbb{R}^n \mid h(x) \geq 0 \}의 전방 불변성(forward invariance)을 보장하는 연속 시간 기법이다.

\dot{h}(x, u) \geq -\alpha(h(x))

여기서 h: \mathbb{R}^n \rightarrow \mathbb{R}은 장벽 함수, u는 제어 입력, \alpha는 클래스 \mathcal{K} 확장 함수이다. 이 조건을 만족하는 제어 입력이 존재하면, 시스템의 상태는 항상 안전 집합 \mathcal{C} 내에 머문다.

임무 관리 문맥에서 CBF는 고수준 임무 제어 명령이 물리적 안전 제약을 위반하지 않도록 필터링하는 안전 필터(safety filter)로 활용된다.

u^* = \arg\min_{u} \; \| u - u_{\text{mission}} \|^2 \quad \text{subject to:} \quad \dot{h}(x, u) \geq -\alpha(h(x))

이 이차 계획 문제(QP)의 해 u^*는 임무 명령 u_{\text{mission}}에 최대한 가까우면서도 안전 제약을 만족하는 제어 입력이다.

6. 확률적 시스템의 형식 검증

6.1 확률적 모델 검사(Probabilistic Model Checking)

센서 불확실성, 통신 손실, 환경 변동 등을 반영하기 위해, 임무 모델을 확률적 시스템으로 구성하고 확률적 속성을 검증한다.

마르코프 결정 과정(MDP)의 확률적 검증: MDP 모델 \mathcal{M}에 대해 확률적 시간 논리 PCTL(Probabilistic Computation Tree Logic)로 명세된 속성을 검증한다.

P_{\geq 0.99}\left[ \Diamond_{\leq T} \text{goal\_reached} \right]: \text{시간 } T \text{ 내 목표 도달 확률이 99\% 이상}

P_{\leq 0.01}\left[ \Diamond \text{collision} \right]: \text{충돌 발생 확률이 1\% 이하}

대표적 확률적 모델 검사 도구로는 PRISM(Kwiatkowska et al., 2011)과 Storm(Dehnert et al., 2017)이 있다.

6.2 보상 기반 속성

확률적 모델 검사는 보상(reward) 기반 속성도 검증할 수 있다. 예를 들어, 임무 완수까지의 기대 에너지 소비를 검증한다.

R_{\leq E_{\max}}\left[ \Diamond \text{mission\_complete} \right]: \text{임무 완수까지의 기대 에너지가 } E_{\max} \text{ 이하}

7. 안전성 보증 체계의 통합

7.1 안전성 보증 케이스(Safety Assurance Case)

형식 검증 결과를 체계적으로 문서화하여 이해관계자에게 안전성을 논증하기 위해, 안전성 보증 케이스(Safety Assurance Case)를 구성한다. GSN(Goal Structuring Notation)(Kelly, 1998)이 대표적 표기법이다.

보증 케이스의 구조는 다음과 같다.

• 최상위 목표(Top-Level Goal): “임무 관리 시스템은 안전하다.”
• 전략(Strategy): “형식 검증을 통해 안전 속성이 보증된다.”
• 증거(Evidence): 모델 검사 결과, 정리 증명 증서, 도달 가능성 분석 보고서
• 가정(Assumption): 환경 모델의 충실도, 센서 정확도의 범위

7.2 DO-178C 및 IEC 61508 준수

항공우주 분야의 DO-178C/DO-333과 산업 안전 표준 IEC 61508은 형식 방법(formal methods)의 적용을 권장하거나 요구한다. 형식 검증 결과는 이러한 인증 표준의 증거로 활용될 수 있다.

8. 한계와 연구 과제

형식 검증의 임무 안전성 적용에서의 주요 한계와 연구 과제는 다음과 같다.

1. 확장성(Scalability): 대규모 다중 로봇 시스템의 결합 상태 공간은 형식 검증의 현재 도구 능력을 초과한다. 조합적 검증, 계약 기반 설계(contract-based design), 계층적 추상화의 발전이 필요하다.

2. 모델 충실도(Model Fidelity): 검증 결과의 현실 적용 가능성은 모델이 실제 시스템을 얼마나 충실히 반영하느냐에 의존한다. 모델과 실 시스템 간의 괴리(gap)를 정량화하는 방법론이 요구된다.

3. 비선형 동역학의 검증: 로봇의 비선형 동역학에 대한 도달 가능성 분석은 계산 비용이 매우 높으며, 과근사의 정밀도가 보수적이 될 수 있다.

4. 학습 기반 구성요소: 심층 신경망을 포함하는 임무 관리 시스템의 형식 검증은 현재 초기 단계에 있다. 신경망의 속성(강건성, 안전성)을 형식적으로 검증하는 연구가 활발히 진행 중이다.

5. 전문성 요구: 정리 증명 기반 검증은 높은 수준의 형식 방법 전문성을 요구하여, 실무 적용의 장벽이 높다. 자동화 수준의 향상과 사용자 친화적 도구의 개발이 과제이다.

9. 참고 문헌

• Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model Checking. MIT Press.
• Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2003). “Counterexample-Guided Abstraction Refinement for Symbolic Model Checking.” Journal of the ACM, 50(5), 752–794.
• Henzinger, T. A. (1996). “The Theory of Hybrid Automata.” Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, 278–292.
• Ames, A. D., Xu, X., Grizzle, J. W., & Tabuada, P. (2017). “Control Barrier Function Based Quadratic Programs for Safety Critical Systems.” IEEE Transactions on Automatic Control, 62(8), 3861–3876.
• Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., … & Maler, O. (2011). “SpaceEx: Scalable Verification of Hybrid Systems.” Computer Aided Verification, Springer.
• Kwiatkowska, M., Norman, G., & Parker, D. (2011). “PRISM 4.0: Verification of Probabilistic Real-Time Systems.” Computer Aided Verification, Springer.
• Kelly, T. P. (1998). “Arguing Safety – A Systematic Approach to Managing Safety Cases.” PhD Thesis, University of York.
• Althoff, M. (2015). “An Introduction to CORA 2015.” Workshop on Applied Verification for Continuous and Hybrid Systems.

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