온라인 게임 서버의 파티 시스템 검증을 위한 스핀 모델 체커 적용에 관한 연구
A Case Study on Model Checking Online-Game Server Party System Using SPIN
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
모델 체킹 방법은 가능한 모든 경우를 자동으로 확인할 수 있으며, 코드가 구현되기 이전의 명세서나 디자인의 검증에도 적용할 수 있어 고위험 시스템의 검증에 활발히 적용되어왔다. 그러나 이러한 엄밀한 검증기법에 대한 일반적인 이해 부족과 테스팅에 비해 높은 검증 비용으로인하여, 일반적인 소프트웨어들은 여전히 인력에 의한 테스팅과 같은 기초적인 방법에 의존하여 검증이 수행되고 있다. 본 논문에서는 그 대표적인 예인 온라인 게임 서버를 대상으로, SPIN 모델 체커(SPIN model checker)를 이용한 자동화 검증 방법을 적용하는 실험적인 연구를 수행하여 검증 비용 대비 효과에 근거한 적용성을 판단하였다. 연구 결과, 5～7GB 이내의 메모리와 10분 이내의 시간 내에서 온라인 게임 서버 파티 시스템의 주요 특성들을 검증할 수 있음을 보였고, 이 과정에서 기존에 파악하지 못한 오류도 검출하였다. 이로부터 인력에 의한 테스팅에비해 납득할만한 수준의 검증 비용으로 엄밀하고 효과적인 검증이 가능하다는 결론을 도출할 수 있었다.
Abstract
Model checking method is able to check all possible cases automatically and is applicable to specifications or design before actual implementation so that some critical systems have adopted this method actively. However, the current practice of software verification is largely dependant on basic methods such as manual testing because of lack of understanding about this rigorous method and high verification cost. In this paper we conducted an experimental research for the automated verification using the SPIN model checker on an online-game server to study the applicability of the technique in this domain. The results show that we could verify major features of the online-game server party system with 5～7 GB memory and within 10 minutes execution time, and also found a hidden system error that passed existing testing process. This result shows the possibility of rigorous and effective verification with reasonable cost in comparison to manual testing.
참고문헌 (17)
- Christel Baier, "Principles of Model Checking", pp.1~2 (2008), The MIT Press
- Nancy Leveson, "Safeware: System Safety and Computers" (1995), Addison-Wesley
- Christel Baier, "Principles of Model Checking", pp.3~6 (2008), The MIT Press
- Edmund M. Clarke, "Model checking" (1999), "The MIT press
- Gerard Holzmann, "The model checker SPIN", IEEE Transactions on Software Engineering, 23(5) (1997)
- "Model checker SPIN"[URL]
- Francis Schneider, "Validating Requirements for Fault Tolerant Systems using Model Checking", Third IEEE Conference on Requirements Engineering (1998)
- Klaus Havelund, "Formal Analysis of the Remote Agent Before and After Flight", Proceedings of the 5th NASA Langley Formal Methods Workshop (2000)
- Yunja Choi, "Model checking Trampoline OS: a case study on safety analysis for automotive software", Softw. Test., Verif. Reliab., pp.38~60 (2014)
- Theo Ruys, "Advanced SPIN Tutorial", Proceedings of the 11th SPIN Workshop (2004)
- Gerard Holzmann, "Software Model Checking", NATO Summer School, 180, pp.309~355 (2000)
- Orna Lichtenstein, "Checking That Finite State Concurrent Programs Satisfy Their Linear Specification", Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp.97~107 (1985)
- Glenford J. Myers, "The Art of Software Testing" (2004), Wiley
- 2013 White Paper on Korean Games, "KOCCA(Korea Creative Content Agency)", ~ (2013)
- "메이플스토리, 아이템 복사 버그 발생…복제 아이템 전량 회수 조치" (2015)[URL]
- "아이템 복사하면 영업방해죄 적용? 최강의 군단, 버그 악용자에 강경대응" (2014)[URL]