모델 체킹 (model checking)
쉽게 풀면
모델 체킹은 시스템이 가질 수 있는 모든 상태와 상태 전이를 하나하나 자동으로 탐색하면서, '이런 나쁜 상태에는 절대 도달하지 않는다'거나 '결국에는 항상 이 상태에 도달한다' 같은 성질이 실제로 성립하는지 검사하는 방법이다. 사람이 직접 증명을 쓰는 정리 증명과 달리 도구가 자동으로 전체 상태 공간을 탐색해준다는 장점이 있지만, 상태의 수가 시스템 크기에 따라 기하급수적으로 폭발하는 '상태 공간 폭발' 문제가 대표적인 한계로 꼽힌다.
왜 중요한가
소프트웨어와 하드웨어 시스템이 복잡해질수록 테스트만으로는 모든 오류 상황을 찾아내기 어려운데, 모델 체킹은 상태 공간을 빠짐없이 탐색해 안전성이나 활성 같은 성질을 수학적으로 보장할 수 있다는 점에서 정형 검증 분야의 핵심 주제로 다뤄집니다. 특히 오류가 생명이나 재산 피해로 이어질 수 있는 항공, 원자력, 금융 시스템, 그리고 병렬성으로 인해 미묘한 버그가 발생하기 쉬운 통신 프로토콜과 하드웨어 회로 검증에서 실무적 요구가 커 관련 연구가 꾸준히 이어지고 있습니다.
논문에서는 이렇게 쓰입니다
하드웨어 회로나 통신 프로토콜의 유한 상태 시스템에 대해 자동화된 검증을 수행했음을 설명할 때 사용된다.
안전이 중요한 임베디드 및 제어 시스템 분야에서는 특정 위험 상태에 절대 도달하지 않는다는 안전 속성 검증에 모델 체킹이 흔히 활용된다.
분산 시스템 분야에서는 여러 노드 간 상호작용으로 발생하는 경쟁 조건이나 합의 실패 가능성을 모델 체킹으로 사전에 확인하는 사례가 많다.
조금 더 깊게 보면
모델 체킹에서 검증 대상 성질은 대체로 시제 논리(temporal logic)로 표현되며, 대표적으로 LTL(선형 시제 논리)과 CTL(분기 시제 논리)이 안전성(어떤 나쁜 일이 절대 일어나지 않음)과 활성(어떤 좋은 일이 결국 일어남) 성질을 기술하는 데 쓰입니다. 상태 공간 폭발 문제를 완화하기 위한 방법으로는 상태를 이진결정다이어그램(BDD)으로 압축해 표현하는 기법이나, 반례를 찾는 데 집중하는 유계 모델 체킹(bounded model checking) 등이 논문에서 자주 언급됩니다. 논문을 읽을 때는 어떤 시제 논리로 성질을 명세했는지, 그리고 상태 공간 폭발을 어떤 방식으로 다루었는지를 함께 살펴보면 연구의 기술적 기여를 파악하는 데 도움이 됩니다.
주의할 점
모델 체킹은 상태 공간이 매우 커지면 계산 자원이 기하급수적으로 늘어나는 상태 공간 폭발 문제를 겪을 수 있어, 대규모 시스템에는 추상화나 근사 기법이 함께 필요하다.