1277.188 SPIN 모델 검사기와 Promela 언어