Model Checker

시스템의 모든 가능한 상태와 동작 경로를 탐색하여 정의된 속성이 위반되는지 자동으로 확인하는 도구.