수학적/논리적인 정형명세에 의해 기술된 시스템의 행위를 유한상태기계(FSM:Finite State Machine)로 모형화하여 모델체킹 도구 를 통해 자동으로 검증하는 방법