모델체킹(Model Checking)이란
정형 명세로 “무엇이 참이어야 하는가”를 적었다면, 모델체킹은 그걸 “정말로 항상 참인지” 자동으로 확인해주는 기법임
기본 아이디어
시스템을 상태(state)와 상태 전이(transition)로 모델링한 뒤, 가능한 모든 상태를 도구가 자동으로 탐색하며 “이 속성이 깨지는 상태가 있는가”를 검사함
상태 A → 상태 B → 상태 C
↘ 상태 D (여기서 속성 위반 발견!)
사람이 모든 경로를 손으로 확인하는 대신, 도구가 상태 공간(state space) 전체를 체계적으로 순회함
검사하는 속성의 두 종류
| 속성 | 의미 | 예시 |
|---|---|---|
| Safety(안전성) | “나쁜 일이 절대 일어나지 않는다” | 두 프로세스가 동시에 임계구역에 못 들어간다 |
| Liveness(활성) | “좋은 일이 언젠가는 반드시 일어난다” | 요청은 결국 언젠가 응답을 받는다 |
이 두 속성을 표현하는 데 시제논리(Temporal Logic, LTL/CTL)가 쓰인다 — “항상(always)”, “언젠가(eventually)” 같은 시간 개념이 들어간 논리식
상태 폭발(State Explosion) 문제
시스템 변수가 늘어날수록 가능한 상태 조합이 기하급수적으로 늘어나서, 현실적인 크기의 시스템은 모든 상태를 다 못 도는 경우가 많음 이를 완화하는 기법(기호적 모델체킹, 추상화)이 이 분야의 핵심 연구 주제 중 하나임
simulation & test 노트와의 차이
시뮬레이션·테스트는 “몇 가지 시나리오를 골라서” 확인하는 표본 검증이고, 모델체킹은 (이론적으로는) 가능한 경로 전체를 확인하는 완전 검증에 가까움 다만 상태 폭발 때문에 실제로는 완전성이 제한될 수 있다는 걸 같이 알아둬야 함
더 생각해볼 것들
- 동시성(parallelism) 노트에서 다룬 경쟁 조건(race condition) 문제를, 모델체킹으로 어떻게 표현하고 잡아낼 수 있을지 예시를 만들어보고 싶음
- 실제로 쓰이는 모델체커(SPIN, TLA+ 등) 중 하나를 가볍게 써보고 싶음