모델 체커로 산타 클로스 동시성 퍼즐 풀기: 실패 사례에서 배우다

Solving Santa Claus Puzzle

벤-아리의 저서에서 영감을 받아, 저자는 산타 클로스 동시성 퍼즐을 SPIN 모델 체커와 Promela로 검증하는 과정을 소개합니다. 이 퍼즐은 산타가 아홉 마리 순록 또는 세 명의 엘프 그룹에 의해 깨어나며, 순록이 우선권을 갖는 동기화 문제입니다. 저자는 먼저 세 가지 잘못된 모델을 의도적으로 설계하여 각각의 실패 시나리오(순록이 모두 준비되지 않았는데 배송, 동시에 배송과 상담, 순록이 대기 중인데 엘프 선택)를 LTL 속성으로 잡아내고, 이를 통해 안전하지 않은 가정을 드러냅니다. 마지막으로 올바른 모델을 제시하고 모델 체커로 검증합니다. 테스트가 놓칠 수 있는 인터리빙을 탐색하는 모델 체커의 장점을 강조합니다.