Àüü
ÀüÀÚ/Àü±â
Åë½Å
ÄÄÇ»ÅÍ
·Î±×ÀÎ
ȸ¿ø°¡ÀÔ
About Us
ÀÌ¿ë¾È³»
¿¬±¸¹®Çå
±¹³» ³í¹®Áö
¿µ¹® ³í¹®Áö
±¹³» ÇÐȸÁö
Çмú´ëȸ ÇÁ·Î½Ãµù
±¹³» ÇÐÀ§ ³í¹®
³í¹®Á¤º¸
¹é¼
±³À°Á¤º¸
¿¬±¸ ù°ÉÀ½
ÇаúÁ¤º¸
°ÀÇÁ¤º¸
µ¿¿µ»óÁ¤º¸
E-Learning
¿Â¶óÀÎ Àú³Î
½ÉÈÁ¤º¸
¿¬±¸ ¹× ±â¼úµ¿Çâ
Áֿ俬±¸ÅäÇÈ
ÁÖ¿ä°úÁ¦ ¹× ±â°ü
Çؿܱâ°ü °ü·ÃÀÚ·á
¹ÙÀÌ¿À Á¤º¸±â¼ú
ÁÖ¿ä Archive Site
Æ÷Ä¿½ºiN
¿¬±¸ÀÚ Á¤º¸
¶óÀÌ¡½ºÅ¸
ÆÄ¿öiNÅͺä
¼¼ÁßÇÑ
¿¬±¸ÀÚ·á
¹®ÀÚ DB
¿ë¾î»çÀü
¾Ë¸²¸¶´ç
ºÎ½Ç ÇмúÈ°µ¿ ¿¹¹æ
³í¹®¸ðÁý
´ëȸ¾È³»
What's New
¿¬±¸ºñÁ¤º¸
±¸ÀÎÁ¤º¸
°øÁö»çÇ×
CSERIC ±¤Àå
Post-Conference
¿¬±¸ÀÚ Ä«Æä
ÀÚÀ¯°Ô½ÃÆÇ
Q&A
´Ý±â
»çÀÌÆ®¸Ê
¿¬±¸¹®Çå
±¹³» ³í¹®Áö
¿µ¹® ³í¹®Áö
±¹³» ÇÐȸÁö
Çмú´ëȸ ÇÁ·Î½Ãµù
±¹³» ÇÐÀ§ ³í¹®
³í¹®Á¤º¸
¹é¼
±³À°Á¤º¸
¿¬±¸ ù°ÉÀ½
ÇаúÁ¤º¸
°ÀÇÁ¤º¸
µ¿¿µ»óÁ¤º¸
E-Learning
¿Â¶óÀÎ Àú³Î
½ÉÈÁ¤º¸
¿¬±¸ ¹× ±â¼úµ¿Çâ
Áֿ俬±¸ÅäÇÈ
ÁÖ¿ä°úÁ¦ ¹× ±â°ü
Çؿܱâ°ü °ü·ÃÀÚ·á
¹ÙÀÌ¿À Á¤º¸±â¼ú
ÁÖ¿ä Archive Site
ÄÄÇ»ÅÍiN
¿¬±¸ÀÚ Á¤º¸
¿¬±¸ÀÚ·á
¹®ÀÚ DB
Ȧ·Î±×·¥ DB
¿ë¾î»çÀü
¾Ë¸²¸¶´ç
ºÎ½Ç ÇмúÈ°µ¿ ¿¹¹æ
³í¹®¸ðÁý
´ëȸ¾È³»
What's New
¿¬±¸ºñ Á¤º¸
±¸ÀÎÁ¤º¸
°øÁö»çÇ×
IT Daily
CSERIC ±¤Àå
Post-Conference
¿¬±¸ÀÚ Ä«Æä
ÀÚÀ¯°Ô½ÃÆÇ
Q&A
¼ºñ½º ¹Ù·Î°¡±â
¼³¹®Á¶»ç
¿¬±¸À±¸®
°ü·Ã±â°ü
Please wait....
¿¬±¸¹®Çå
±¹³» ³í¹®Áö
¿µ¹® ³í¹®Áö
±¹³» ÇÐȸÁö
Çмú´ëȸ ÇÁ·Î½Ãµù
±¹³» ÇÐÀ§ ³í¹®
³í¹®Á¤º¸
¹é¼
±¹³» ³í¹®Áö
Ȩ > ¿¬±¸¹®Çå > ±¹³» ³í¹®Áö >
Çѱ¹Á¤º¸Ã³¸®ÇÐȸ ³í¹®Áö
>
Á¤º¸Ã³¸®ÇÐȸ ³í¹®Áö ¼ÒÇÁÆ®¿þ¾î ¹× µ¥ÀÌÅÍ °øÇÐ
Á¤º¸Ã³¸®ÇÐȸ ³í¹®Áö ¼ÒÇÁÆ®¿þ¾î ¹× µ¥ÀÌÅÍ °øÇÐ
Current Result Document :
1
/ 6
´ÙÀ½°Ç
ÇѱÛÁ¦¸ñ(Korean Title)
¿Â¶óÀÎ °ÔÀÓ ¼¹öÀÇ ÆÄƼ ½Ã½ºÅÛ °ËÁõÀ» À§ÇÑ ½ºÇÉ ¸ðµ¨ üĿ Àû¿ë¿¡ °üÇÑ ¿¬±¸
¿µ¹®Á¦¸ñ(English Title)
A Case Study on Model Checking Online-Game Server Party System Using SPIN
ÀúÀÚ(Author)
Goanghun Kim
Yunja Choi
±è±¤ÈÆ
ÃÖÀ±ÀÚ
¿ø¹®¼ö·Ïó(Citation)
VOL 04 NO. 11 PP. 0479 ~ 0486 (2015. 11)
Çѱ۳»¿ë
(Korean Abstract)
¸ðµ¨ üŷ ¹æ¹ýÀº °¡´ÉÇÑ ¸ðµç °æ¿ì¸¦ ÀÚµ¿À¸·Î È®ÀÎÇÒ ¼ö ÀÖÀ¸¸ç, Äڵ尡 ±¸ÇöµÇ±â ÀÌÀüÀÇ ¸í¼¼¼³ª µðÀÚÀÎÀÇ °ËÁõ¿¡µµ Àû¿ëÇÒ ¼ö ÀÖ¾î °íÀ§Çè ½Ã½ºÅÛÀÇ °ËÁõ¿¡ È°¹ßÈ÷ Àû¿ëµÇ¾î¿Ô´Ù. ±×·¯³ª ÀÌ·¯ÇÑ ¾ö¹ÐÇÑ °ËÁõ±â¹ý¿¡ ´ëÇÑ ÀϹÝÀûÀÎ ÀÌÇØ ºÎÁ·°ú Å×½ºÆÿ¡ ºñÇØ ³ôÀº °ËÁõ ºñ¿ëÀ¸·Î ÀÎÇÏ¿©, ÀϹÝÀûÀÎ ¼ÒÇÁÆ®¿þ¾îµéÀº ¿©ÀüÈ÷ Àη¿¡ ÀÇÇÑ Å×½ºÆðú °°Àº ±âÃÊÀûÀÎ ¹æ¹ý¿¡ ÀÇÁ¸ÇÏ¿© °ËÁõÀÌ ¼öÇàµÇ°í ÀÖ´Ù. º» ³í¹®¿¡¼´Â ±× ´ëÇ¥ÀûÀÎ ¿¹ÀÎ ¿Â¶óÀÎ °ÔÀÓ ¼¹ö¸¦ ´ë»óÀ¸·Î, SPIN ¸ðµ¨ üĿ(SPIN model checker)¸¦ ÀÌ¿ëÇÑ ÀÚµ¿È °ËÁõ ¹æ¹ýÀ» Àû¿ëÇÏ´Â ½ÇÇèÀûÀÎ ¿¬±¸¸¦ ¼öÇàÇÏ¿© °ËÁõ ºñ¿ë ´ëºñ È¿°ú¿¡ ±Ù°ÅÇÑ Àû¿ë¼ºÀ» ÆÇ´ÜÇÏ¿´´Ù. ¿¬±¸ °á°ú, 5¢¦7GB À̳»ÀÇ ¸Þ¸ð¸®¿Í 10ºÐ À̳»ÀÇ ½Ã°£ ³»¿¡¼ ¿Â¶óÀÎ °ÔÀÓ ¼¹ö ÆÄƼ ½Ã½ºÅÛÀÇ ÁÖ¿ä Ư¼ºµéÀ» °ËÁõÇÒ ¼ö ÀÖÀ½À» º¸¿´°í, ÀÌ °úÁ¤¿¡¼ ±âÁ¸¿¡ ÆľÇÇÏÁö ¸øÇÑ ¿À·ùµµ °ËÃâÇÏ¿´´Ù. À̷κÎÅÍ Àη¿¡ ÀÇÇÑ Å×½ºÆÿ¡ ºñÇØ ³³µæÇÒ¸¸ÇÑ ¼öÁØÀÇ °ËÁõ ºñ¿ëÀ¸·Î ¾ö¹ÐÇÏ°í È¿°úÀûÀÎ °ËÁõÀÌ °¡´ÉÇÏ´Ù´Â °á·ÐÀ» µµÃâÇÒ ¼ö ÀÖ¾ú´Ù.
¿µ¹®³»¿ë
(English 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.
Å°¿öµå(Keyword)
SPIN Model Checker
Online Game Server Verification
½ºÇÉ ¸ðµ¨ üĿ
¿Â¶óÀÎ °ÔÀÓ ¼¹ö °ËÁõ
ÆÄÀÏ÷ºÎ
PDF ´Ù¿î·Îµå
¸ñ·Ï
Copyright(c)
Computer Science Engineering Research Information Center
. All rights reserved.