Ȩ > Ç¥ÁØÈ °³¿ä > TTAÀÇ Ç¥ÁØÇöȲ
Ç¥ÁعøÈ£ | [ÆóÁö] TTAK.KO-11.0160 | ±¸Ç¥ÁعøÈ£ | |
---|---|---|---|
Á¦°³Á¤ÀÏ | 2013-12-18 | ÃÑÆäÀÌÁö | 30 |
ÇѱÛÇ¥Áظí | ÀÓº£µðµå ¼ÒÇÁÆ®¿þ¾î Á¤Çü °ËÁõ ÀýÂ÷ Áöħ | ||
¿µ¹®Ç¥Áظí | Guideline for Process of Formal Verification in Embedded Software | ||
Çѱ۳»¿ë¿ä¾à | º» Ç¥ÁØÀº Á¤Çü ¸í¼¼ ¹× °ËÁõÀÇ ÀýÂ÷¸¦ Á¤ÀÇÇÏ°í °ËÁõ °á°ú¸¦ Æò°¡ÇÏ´Â ¹æ¹ýÀ» Á¤ÀÇÇÑ´Ù. ù° ¿ä±¸ »çÇ× Á¤Çü ¸í¼¼ ÀýÂ÷¿Í ¹æ¹ýÀ» ¼³¸íÇÏ°í, ¿ä±¸ »çÇ× ÀÛ¼º ÅÛÇø´ Á¦°øÇÑ´Ù. µÑ°, Á¤Çü °ËÁõÀ» À§ÇÑ ¸ðµ¨¸µ ÀýÂ÷¸¦ Á¤ÀÇÇÏ°í ¸ðµ¨¸µ ÀÛ¼º ÅÛÇø´À» Á¦°øÇÑ´Ù. ¼Â°, Á¤Çü ¸í¼¼µÈ ¿ä±¸ »çÇ×°ú ½Ã½ºÅÛ ¸ðµ¨·ÎºÎÅÍ Á¤Çü °ËÁõÇÏ´Â ÀýÂ÷¸¦ Á¤ÀÇÇÏ°í °ËÁõ °á°ú¸¦ ÀÛ¼ºÇÏ´Â ÅÛÇø´À» Á¦°øÇÑ´Ù. ¸¶Áö¸·À¸·Î ÇØ´ç Á¤Çü °ËÁõÀÇ Àüü °úÁ¤À» Æò°¡ÇÏ´Â ¹æ¹ýÀ» Á¤ÀÇÇÑ´Ù. | ||
¿µ¹®³»¿ë¿ä¾à | This standard defines the processes of the formalization of requirements and formal verification, and provides the evaluation methods for results of the verification. First, we explain the processes and methods about formalizing given requirements and provide the template for writing the formal requirements. Second, we define the process to model the given system to be formally verified and give the template for the model. Third, we define the process of formally verifying the system model with the formal requirements and give the template also. Finally, we define the method for evaluate the whole processes. | ||
±¹Á¦Ç¥ÁØ | |||
°ü·ÃÆÄÀÏ | TTAK.KO-11.0160.pdf |