http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
박사천(Sachoun Park),이건수(Gunsoo Lee),권기현(Gihwon Kwon) 한국정보과학회 2008 한국정보과학회 학술발표논문집 Vol.35 No.1
SPIN은 소프트웨어 정확성 검사에 널리 사용되는 모델 검증 도구이다. 특히 C 코드로 작성된 소프트웨어를 효율적으로 검사하기 위해서 SPIN의 입력 언어인 Promela 모델에 C 코드를 끼워 넣는 기능이 버전 4.0 이상에서 지원되고 있다. 본 논문에서는 이러한 기능을 미로 게임 풀이에 적용하였다. 그 결과, Promela 모델만을 사용해서 풀이한 것보다도 모델에 C 코드를 끼워 풀이한 것이 메모리 사용 및 처리 시간에서 월등히 우수했다. 메모리와 시간과 같은 객관적인 성능 향상과 더불어서, 이러한 사례 연구는 모델 검증 도구 및 추상화 학습에도 유용함을 경험했다.
박사천 ( Sachoun Park ),이건수 ( Gunsoo Lee ),권기현 ( Gihwon Kwon ) 한국정보처리학회 2008 한국정보처리학회 학술대회논문집 Vol.15 No.1
본 논문은 게임 풀이를 통해서 모델 체킹 도구의 특징을 분석한다. 도망자-추적자 게임은 격자 모양의 미로에서 도망자가 추적자를 따돌리고 탈출하는 게임이다. 도망자가 격자 상에서 한 칸 움직일 때, 추적자는 일정한 패턴을 가지고 두 칸 움직인다. 이 문제를 SMV 와 SPIN 모델 체커로 모델링하고 검증하는 과정을 통해서 SMV 와 Spin 모델 체커의 특징을 분석한다. 실험을 통해서 우리는 최단 경로를 찾을 경우는 SMV 모델 체커를 사용해야 하고, 가능한 경로를 빨리 찾는 경우는 Spin 모델 체커가 더 적합함을 확인할 수 있었다.