Model Checking

**Model Checking(모델 검증)**이란, 형식적으로 명세된 시스템 모델이 요구사항을 만족하는지 자동으로 검증하는 기법입니다. 하드웨어, 소프트웨어, 통신 프로토콜, 임베디드 시스템 등에서 사용됩니다.


---

핵심 구성 요소:

모델(Model): 시스템의 상태 전이 구조 (예: Kripke 구조)

명세(Specification): 요구사항을 표현한 논리식 (보통 LTL, CTL 등)

검증 엔진(Checker): 모델이 명세를 만족하는지 자동으로 판정



---

작동 방식:

1. 시스템을 상태 전이 시스템으로 모델링
(예: 어떤 상태에서 어떤 조건에 따라 다음 상태로 전이됨)


2. 요구사항을 형식 논리로 기술
(예: "항상 오류 상태에 빠지지 말 것" → AG ¬error)


3. 검증 도구가 모든 가능한 실행 경로를 탐색하며
명세 만족 여부를 자동 확인


4. 위반이 발견되면 반례(counterexample) 제공
(즉, 요구사항을 위반하는 실행 경로를 보여줌)




---

장점:

자동화됨

반례 제공으로 디버깅 용이

수학적으로 엄밀


단점:

상태 공간 폭발(state explosion) 문제가 있음

복잡한 시스템일수록 모델링이 어렵고 리소스 많이 소모



---

대표 도구:

NuSMV (LTL, CTL 지원)

Spin (LTL 전용)

UPPAAL (시간 제약 시스템용)

TLA⁺/TLC, Alloy, PRISM



---

요약:

즉, Model Checking은 시스템의 모든 가능한 동작을 검사해 논리적 요구사항을 만족하는지 자동으로 판별해주는 수학적 검증 기법입니다.