1277.71 모델 검사와 유한 상태 머신