A Case Study on Model Checking Online-Game Server Party System Using SPIN


KIPS Transactions on Software and Data Engineering, Vol. 4, No. 11, pp. 479-486, Nov. 2015
10.3745/KTSDE.2015.4.11.479,   PDF Download:

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.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
G. Kim and Y. Choi, "A Case Study on Model Checking Online-Game Server Party System Using SPIN," KIPS Transactions on Software and Data Engineering, vol. 4, no. 11, pp. 479-486, 2015. DOI: 10.3745/KTSDE.2015.4.11.479.

[ACM Style]
Goanghun Kim and Yunja Choi. 2015. A Case Study on Model Checking Online-Game Server Party System Using SPIN. KIPS Transactions on Software and Data Engineering, 4, 11, (2015), 479-486. DOI: 10.3745/KTSDE.2015.4.11.479.