Spin을 이용한 근사 정렬된 우선 순위 큐 스케줄러 알고리즘의 명세 정형기법