Á¤º¸°úÇÐȸ³í¹®Áö (Journal of KIISE)
Current Result Document :
ÇѱÛÁ¦¸ñ(Korean Title) |
Coq¿¡¼ÀÇ ½Ç½Ã°£ ºÐ»ê ½Ã½ºÅÛ °ËÁõÀ» À§ÇÑ ³×Æ®¿öÅ© ¹× ¿î¿µÃ¼Á¦ ÇൿÀÇ Á¤Çü ¸ðµ¨ Á¤ÀÇ |
¿µ¹®Á¦¸ñ(English Title) |
Formal Model Design for Network and Operating System Behaviors in Real-time Distributed System Verification with Coq |
ÀúÀÚ(Author) |
±èÀ±½Â
ÇãÃæ±æ
Yoonseung Kim
Chung-Kil Hur
|
¿ø¹®¼ö·Ïó(Citation) |
VOL 47 NO. 11 PP. 1071 ~ 1077 (2020. 11) |
Çѱ۳»¿ë (Korean Abstract) |
Á¤Çü °ËÁõÀ» Àû¿ëÇÏ¿© ºÐ»ê ½Ã½ºÅÛÀÇ ¾ÈÀü¼ºÀ» ³ôÀÌ´Â °ÍÀº Áß¿äÇÑ °úÁ¦ÀÌ´Ù. ºÐ»ê ½Ã½ºÅÛ Áß Ç×°ø, ÀÇ·á±â±â¿Í °°Àº ¾ÈÀü ¿ì¼± ½Ã½ºÅÛÀº ¾ÈÀü¼ºÀÇ À§ÇùÀÌ Å« »ç°í¿Í Á÷°áµÉ ¼ö ÀÖ´Ù. ÇÏÁö¸¸ ºÐ»ê ½Ã½ºÅÛÀ» Á¤Çü °ËÁõÇϱâ À§Çؼ´Â ¼ÒÇÁÆ®¿þ¾îÀÇ ½ÇÇà Àǹ̻Ӹ¸ ¾Æ´Ï¶ó, ¼ÒÇÁÆ®¿þ¾î¸¦ ½ÇÇà½ÃÅ°´Â ¿î¿µÃ¼Á¦¿Í ¸Þ½ÃÁö¸¦ Àü´ÞÇÏ´Â ³×Æ®¿öÅ©ÀÇ È¯°æ µî¿¡ ´ëÇÑ ±â¼úÀÌ ÇÊ¿äÇÏ´Ù. ¿ì¸®´Â Coq Áõ¸í º¸Á¶ µµ±¸ ¾È¿¡¼ ³×Æ®¿öÅ©¿Í ¿î¿µÃ¼Á¦ÀÇ Ãß»óÀûÀÎ Çൿ¿¡ ´ëÇÑ ¸ðµ¨À» Á¤ÀÇÇÏ¿´´Ù. ÀÌ ¸ðµ¨Àº ´Ü°èÀûÀ¸·Î ³×Æ®¿öÅ© °¢ Áö¿ªÀÇ ½ÇÇà ±ÔÄ¢À» Á¦½ÃÇÏ°í, À̷κÎÅÍ Àüü ½Ã½ºÅÛÀÇ ÇൿÀ» ±¸¼ºÇÑ´Ù. ¿ì¸®´Â ÀÌ ¸ðµ¨ÀÌ ½ÇÁ¦·Î ºÐ»ê ½Ã½ºÅÛ °ËÁõ¿¡ À¯¿ëÇÏ°Ô »ç¿ëµÉ ¼ö ÀÖÀ½À» º¸À̱â À§ÇØ °£´ÜÇÑ ¼¹ö-Ŭ¶óÀ̾ðÆ® ½Ã½ºÅÛ °ËÁõÀ» ¼öÇàÇÏ¿´À¸¸ç, ÀÌÈÄ ½Ç¿ëÀûÀÎ ¼ÒÇÁÆ®¿þ¾î °ËÁõ¿¡ Àû¿ëµÇ±â¸¦ ±â´ëÇÏ°í ÀÖ´Ù. |
¿µ¹®³»¿ë (English Abstract) |
Improving the safety and reliability of distributed systems using formal verification methods is an urgent problem. As many of these distributed systems are safety-critical, such as medical or avionics systems, failures of these systems may cause catastrophic results. However, applying formal verification to distributed systems requires not only execution semantics in software, but also behavioral models of the environments, including the operating systems and network involved. We designed a formal abstract model of network and operating system behaviors with the Coq proof assistant. This model consists of local-site execution semantics that model a single computer, the composition of these local-site semantics along with a message exchange model constitutes the global system semantics. We applied and tested this model to verify its applicability when used in a simple server-client system. We expect this model to be used in the verification of practical systems. |
Å°¿öµå(Keyword) |
¼ÒÇÁÆ®¿þ¾î Á¤Çü °ËÁõ
ºÐ»ê ½Ã½ºÅÛ
½Ç½Ã°£ ½Ã½ºÅÛ
Á¤Çü ¸ðµ¨
software formal verification
distributed systems
real-time systems
formal model
|
ÆÄÀÏ÷ºÎ |
PDF ´Ù¿î·Îµå
|