Á¤º¸°úÇÐȸ³í¹®Áö (Journal of KIISE)
ÇѱÛÁ¦¸ñ(Korean Title) |
¿ì¼±¼øÀ§ ±â¹Ý ¸ÖƼŽºÅ© ÇÁ·Î±×·¥ÀÇ API È£Ãâ ¾ÈÀü¼º °ËÁõÀ» À§ÇÑ ¸ðµ¨ ±â¹Ý ¿À°æº¸ ½Äº° ±â¹ý |
¿µ¹®Á¦¸ñ(English Title) |
False-alarm Detection in Model-based API-call Safety Checking of Priority-based Multitasking Programs |
ÀúÀÚ(Author) |
±èµ¿¿ì
ÃÖÀ±ÀÚ
Dongwoo Kim
Yunja Choi
|
¿ø¹®¼ö·Ïó(Citation) |
VOL 46 NO. 10 PP. 1035 ~ 1043 (2019. 10) |
Çѱ۳»¿ë (Korean Abstract) |
¸ÖƼŽºÅ© ÇÁ·Î±×·¥Àº ´Ù¼öÀÇ Å½ºÅ©°¡ ¿î¿µÃ¼Á¦ÀÇ ½ºÄÉÁÙ¸µ¿¡ ¸ÂÃß¾î ¹ø°¥¾Æ ¼öÇàµÇ´Â ÇÁ·Î±×·¥ÀÌ´Ù. ¸ÖƼŽºÅ© ÇÁ·Î±×·¥À» °ËÁõÇϱâ À§Çؼ´Â ¿î¿µÃ¼Á¦ÀÇ ÇàÀ§¸¦ °í·ÁÇؾßÇÏ¸ç ±×·¸Áö ¾ÊÀ» °æ¿ì ¿ì¼±¼øÀ§°¡ ³·Àº ŽºÅ©°¡ ¸ÕÀú ½ÇÇàµÇ´Â µî ¿À°æº¸°¡ ¹ß»ýÇÑ´Ù. È¿°úÀûÀÎ ¸ÖƼŽºÅ© ÇÁ·Î±×·¥ °ËÁõÀ» À§ÇØ Á¤Çü ¿î¿µÃ¼Á¦ ¸ðµ¨À» »ç¿ëÇÑ ¸ðµ¨ °ËÁõ ¹æ¹ýµéÀÌ ¼Ò°³µÇ¾úÀ¸³ª À̵éÀº ÇÁ·Î±×·¥À» Ãß»óÈÇÔÀ¸·Î ÀÎÇØ ¿À°æº¸¸¦ º¸°íÇÒ ¼ö ÀÖ´Ù´Â ´ÜÁ¡ÀÌ ÀÖ´Ù. º» ¿¬±¸¿¡¼´Â ¸ðµ¨ °ËÁõ °á°ú º¸°íµÈ ¹Ý·ÊÀÇ ¿À°æº¸ ¿©ºÎ¸¦ ½Äº°Çϱâ À§ÇÏ¿© ¹Ý·Ê¿Í µ¿ÀÏÇÑ ¼ø¼·Î API ÇÔ¼ö È£ÃâÀ» ¼öÇàÇÏ´Â ÇÁ·Î±×·¥ ½ÇÇà °æ·ÎÀÇ Á¸Àç ¿©ºÎ¸¦ ÄÚµå°ËÁõ ±â¹ýÀ» ÀÌ¿ëÇÏ¿© È®ÀÎÇÏ´Â ¹æ¹ýÀ» ¼Ò°³ÇÑ´Ù. º» ¿¬±¸ÀÇ È¿°ú¸¦ ÀÔÁõÇϱâ À§ÇØ Â÷·®ÀüÀå¿ë ¿î¿µÃ¼Á¦¸¦ À§ÇÑ Å×½ºÆ® ÇÁ·Î±×·¥°ú Â÷·®ÀüÀå¿ë â¹® Á¦¾î ÇÁ·Î±×·¥À» °ËÁõÇÏ°í º¸°íµÈ ¹Ý·ÊÀÇ ¿À°æº¸ ¿©ºÎ¸¦ ½Äº°ÇÑ °á°ú 73%´Â ¿À°æº¸ÀÓÀ» È®ÀÎÇÏ¿´À¸¸ç °¢°¢ Æò±Õ 0.199ÃÊ¿Í 17.95ÃÊÀÇ ½Äº° ½Ã°£ÀÌ ¼Ò¿äµÇ¾ú´Ù.
|
¿µ¹®³»¿ë (English Abstract) |
A multitask program consists of a set of tasks that are executed according to a scheduling policy of the operating system. In order to verify a multitask program, it is necessary to consider the behavior of the operating system. Otherwise, false alarms are reported, e.g., a low-priority task is executed prior to a higher-priority task. Studies introduced a model-based verification method using the formal OS model for the effective verification of multitask programs, but they showed high false-alarm rates due to the abstraction of the application program. This paper proposes an automated false-alarm detection method which identifies false alarms by checking existence of the program path that performs the same sequence of API-calls as the counterexample reported by the model-based verification. The suggested method is applied to two sets of application programs running on an automotive operating system. Results show that 73% of the reported counterexamples were false alarms with an average detection time of 0.199 seconds for the test program and 17.95 seconds for the window control program.
|
Å°¿öµå(Keyword) |
API
API È£Ãâ Á¦¾à»çÇ× °ËÁõ
Á¤Çü °ËÁõ
¿À°æº¸ ½Äº°
API
API-call constraint checking
formal verification
false-alarm detection
|
ÆÄÀÏ÷ºÎ |
PDF ´Ù¿î·Îµå
|