- Äɲ䵤줿¹Ô¤Ï¤³¤Î¿§¤Ç¤¹¡£
- ºï½ü¤µ¤ì¤¿¹Ô¤Ï¤³¤Î¿§¤Ç¤¹¡£
- ¸¦µæ¥Æ¡¼¥Þ/¸¡¾Ú ¤Ø¹Ô¤¯¡£
*·Á¼°Åª¸¡¾Ú [#c1bdf663]
**¥Æ¥¹¥È¤È¸¡¾Ú [#i308b1db]
ºîÀ®¤·¤¿¥×¥í¥°¥é¥à¤Ë¸í¤ê¤¬¤Ê¤¤¤«³Î¤«¤á¤ëÊýË¡¤È¤·¤Æ¡¤¼ç¤Ë''¥Æ¥¹¥È''¤È''¸¡¾Ú''¤¬¤¢¤ê¤Þ¤¹¡¥
''¥Æ¥¹¥È''(test)¤È¤Ï¡¤¼ÂºÝ¤Ë¥×¥í¥°¥é¥à¤ò¼Â¹Ô¤·¡¤·ë²Ì¤¬´üÂÔÄ̤꤫¤É¤¦¤«´Ñ»¡¤¹¤ë¤³¤È¤Ç¤¹¡¥¤â¤Á¤í¤ó¡¤1¡Á2Ä̤ê»î¤·¤¿¤À¤±¤Ç¸í¤ê¤¬¤Ê¤¤¤È¤ÏÊݾڤǤ¤Ê¤¤¤Î¤Ç¡¤Àø¤ó¤Ç¤¤¤ë¸í¤ê¤ò¤Ê¤ë¤Ù¤¯¤¿¤¯¤µ¤ó¸«¤Ä¤±¤é¤ì¤ë¤è¤¦¡¤¥Æ¥¹¥ÈÆâÍƤòÀ߷פ¹¤ëɬÍפ¬¤¢¤ê¤Þ¤¹¡Ê¤½¤ÎÊýË¡¤Ë¤Ä¤¤¤Æ¤ÏÎ㤨¤Ð²¼µÊ¸¸¥¤Ê¤É¡Ë¡¥¤·¤«¤·¤½¤ì¤Ç¤â¡¤¥¿¥¤¥ß¥ó¥°¤Ëµ¯°ø¤¹¤ë¸í¤ê¡¤ÌÇ¿¤Ë¤¢¤é¤ï¤Ë¤Ê¤é¤Ê¤¤¸í¤ê¡¤¶öÁ³¤¬½Å¤Ê¤Ã¤Æ¤¢¤é¤ï¤Ë¤Ê¤ë¸í¤ê¤Ê¤É¤Ï¡¤¥Æ¥¹¥È¤Çȯ¸«¤¹¤ë¤³¤È¤¬º¤Æñ¤Ç¤¹¡¥
//¤·¤«¤·¡¤¤½¤ì¤Ç¤â¡Ö¤É¤Î¤è¤¦¤ÊÆþÎϤËÂФ·¤Æ¤â´üÂÔÄ̤ê¤ÎÆ°ºî¤ò¤¹¤ë¡×¤³¤È¤òÊݾڤ¹¤ë¤Î¤Ïº¤Æñ¤Ç¤¹¡¥
-G.J.Myers¤Û¤«¡Ø¥½¥Õ¥È¥¦¥§¥¢¡¦¥Æ¥¹¥È¤Îµ»Ë¡¡ÙÂè2ÈÇ, ĹÈø ´ÆÌõ, ¾¾Èø Ìõ, ¶áÂå²Ê³Ø¼Ò, 2006.
-¶Ì°æ, »°Åè, ¾¾ÅÄ¡Ø¥½¥Õ¥È¥¦¥§¥¢¤Î¥Æ¥¹¥Èµ»Ë¡¡Ù¶¦Î©½ÐÈÇ, 1988.
**¥â¥Ç¥ë¸¡ºº [#yf989a0e]
¥Æ¥¹¥È¤Ç¤Ï¸«¤Ä¤±¤Ë¤¯¤¤¸í¤ê¤ò¸«¤Ä¤±¤ë¤¿¤á¤Ë¡¤¡ÖÁ´¤Æ¤ÎÁȹ礻¤òµ¡³£¤Ë»î¤µ¤»¤Æ¡¤¥¨¥é¡¼¾õÂÖ¤ËÅþ㤹¤ë¤«¤É¤¦¤«Ä´¤Ù¤ë¡×¤È¤¤¤¦ÊýË¡¤¬¤¢¤ê¤Þ¤¹¡¥¤³¤ì¤¬''¥â¥Ç¥ë¸¡ºº'' (model-checking) ¤Ç¤¹¡¥
-¥¨¥é¡¼¾õÂÖ¤ÎÎã
--¥Ì¥ë¥Ý¥¤¥ó¥¿»²¾È
--¥Ç¥Ã¥É¥í¥Ã¥¯
--¥×¥í¥°¥é¥àÃæ¤Î»ØÄꤵ¤ì¤¿°ÌÃÖ
ERROR: ...
--»ØÄꤵ¤ì¤¿ÏÀÍý¼°¤ÎÉÔÀ®Î©
assert(x > 0); // x <= 0 ¤Ê¤é¤Ð¥¨¥é¡¼
--¤Ê¤É¤Ê¤É
-[[CPAchecker¤Ë¤è¤ë´Êñ¤Ê¸¡¾ÚÎã>¥á¥ó¥Ð¡¼/y-takata/CPAchecker#example]]
¥Æ¥¹¥È¤È¤Á¤¬¤¦¤Î¤Ï¡ÖÆþÎϤÎÁ´Áȹ礻¤ò¹Íθ¤·¤Æ·ë²Ì¤ò½Ð¤·¤Æ¤¤¤ë¡×¤È¤¤¤¦ÅÀ¤Ç¤¹¡¥
***Ãê¾Ý²½¤ÈÌÏ·¿ [#v8e4844d]
¤½¤¦Ê¹¤¯¤È¡¤¼¡¤Î¤è¤¦¤Êµ¿Ì䤬¤ï¤¯¤«¤âÃΤì¤Þ¤»¤ó¡¥¡Öint·¿¤¬32¥Ó¥Ã¥È¤À¤È¤¹¤ë¤È¡¤Î㤨¤Ð3¤Ä¤ÎÀ°¿ô¤òÆþÎϤȤ¹¤ë¥×¥í¥°¥é¥à¤Ç¤ÏÁȹ礻¤ÏÌó 43²¯¤Î3¾è Ä̤ꡥ¸½¼ÂŪ¤Ê»þ´Ö¤ÇÁ´Áȹ礻¤òÄ´¤Ù¤é¤ì¤ë¤Ï¤º¤¬¤Ê¤¤¤Î¤Ç¤Ï?¡×
¤Þ¤Ã¤¿¤¯¤½¤ÎÄ̤ê¤Ç¡¤ËÜÅö¤ËÁ´¤Æ¤ÎÁȹ礻¤ò»î¤·¤Æ¤¤¤¿¤Î¤Ç¤Ï¡¤¤É¤ì¤À¤±»þ´Ö¤ò³Ý¤±¤Æ¤â¸¡¾Ú¤Ç¤¤Þ¤»¤ó¡¥¼ÂºÝ¤Ï¡¤''Ãê¾Ý²½'' (abstraction) ¤È¤¤¤¦µ»½Ñ¤ò»È¤Ã¤Æ¥×¥í¥°¥é¥à¤òñ½ã²½¤·¡¤¤½¤ì¤ÇÆÀ¤é¤ì¤¿''ÌÏ·¿'' (model) ¤ò»È¤Ã¤Æ¡¤¥¨¥é¡¼¾õÂÖ¤ËÅþ㤹¤ë¤«¤É¤¦¤«¤òÄ´¤Ù¤Þ¤¹¡¥Ãê¾Ý²½¤È¤Ï¡¤Î㤨¤Ð¡Ö³ÆÊÑ¿ô¤ò 0 ¤Þ¤¿¤Ï 1 ¤Î1¥Ó¥Ã¥È¤Ëñ½ã²½¤¹¤ë¡×¤È¤¤¤Ã¤¿Áàºî¤Ç¤¹¡¥
#br
¸½¼ÂŪ¤Ê»þ´Ö¤Ç¼«Æ°¸¡¾Ú¤ò¹Ô¤¦¤¿¤á¤Ë¤ÏÃê¾Ý²½¤¬É¬ÍפǤ¹¤¬¡¤°ìÊý¡¤Ãê¾Ý²½¤Î¤¿¤á¤Ë¸¡¾Ú·ë²Ì¤¬ÉÔÀµ³Î¤Ë¤Ê¤ë¡Ê¤¹¤Ê¤ï¤Á¡¤¸µ¤Î¥×¥í¥°¥é¥à¤Ï°ÂÁ´¤Ê¤Î¤Ë¡¤ÌÏ·¿¤Ï¡Ö¥¨¥é¡¼¾õÂÖ¤ËÅþ㤹¤ë¡×¤ÈȽÄꤵ¤ì¤ë¡Ë¤³¤È¤¬¤¢¤ê¤Þ¤¹¡ÊÎ㤨¤Ð[[¤³¤Á¤é¤Î¸¡¾ÚÎã>¥á¥ó¥Ð¡¼/y-takata/CPAchecker#example]]¤ÎÎã2¡Ë¡¥¤·¤«¤â¡¤¤½¤Î¤è¤¦¤Ê¥º¥ì¤Îµ¯¤¤Ê¤¤100%Àµ³Î¤Ê¼«Æ°¸¡¾Ú¤ò¹Ô¤¦¤³¤È¤Ï¡¤ÍýÏÀŪ¤ËÉÔ²Äǽ¤Ç¤¢¤ë¤³¤È¤¬¤ï¤«¤Ã¤Æ¤¤¤Þ¤¹((Ää»ßÀÌäÂ꤬·èÄêÉÔǽ¤Ç¤¢¤ë¤³¤È¤«¤éÍưפˤ狼¤ê¤Þ¤¹¡¥))¡¥½¾¤Ã¤Æ¡¤¸¡¾Ú¤·¤è¤¦¤È»×¤Ã¤Æ¤¤¤ë»öÊÁ¤ò¤Ê¤ë¤Ù¤¯Àµ³Î¤Ë°·¤¨¤Æ¤«¤Ä¼«Æ°¸¡¾Ú¤¬²Äǽ¤Ê¡¤Å¬ÀÚ¤ÊÃê¾Ý²½¤ò»Ü¤¹¤³¤È¤¬¡¤¥â¥Ç¥ë¸¡ºº¼êË¡¤Î¸°¤È¤Ê¤ê¤Þ¤¹¡¥
//¡ÖÌÏ·¿¤¬ SAFE ¤Ê¤é¡¤¸µ¤Î¥×¥í¥°¥é¥à¤â°ÂÁ´¡×¤È¤¤¤¦¤³¤È¤ÏÊݾڤǤ¤Þ¤¹¤Î¤Ç¡¤¥â¥Ç¥ë¸¡ºº¤¬Ìò¤ËΩ¤¿¤Ê¤¤¤ï¤±¤Ç¤Ï¤¢¤ê¤Þ¤»¤ó¤¬¡¤¤Ê¤ë¤Ù¤¯¡Ö°ÂÁ´¤Ç¤¢¤ì¤Ð°ÂÁ´¤ÈȽÄꤵ¤ì¤ë¡×¤Î¤¬Ë¾¤Þ¤·¤¤¤È¤³¤í¤Ç¤¹¡¥¤·¤«¤·¡¤¼Â¤Ï¡Ö100%¤½¤Î¤è¤¦¤Ë¤¹¤ë¤³¤È¤ÏÉÔ²Äǽ¡×¤Ç¤¢¤ë¤³¤È¤¬¤ï¤«¤Ã¤Æ¤¤¤Þ¤¹¡¥
#br
¸¦µæ¼¼¤Ç¤Ï¡Ö¾ðÊó¥Ù¡¼¥¹¥¢¥¯¥»¥¹À©¸æ(IBAC)¤Î¤¿¤á¤Î¥â¥Ç¥ë¸¡ººË¡¡×¤Î¤è¤¦¤Ê¡Ö¡û¡û¤Î¤¿¤á¤Î¥â¥Ç¥ë¸¡ººË¡¤Î¸¦µæ¡×¤È¤¤¤¦¥¿¥¤¥×¤Î¸¦µæ¥Æ¡¼¥Þ¤ò¤³¤ì¤Þ¤Ç¤Ë¤¤¤¯¤Ä¤«°·¤¤¤Þ¤·¤¿¡¥¡Ö¡û¡û¡×¤ËÆþ¤ë¤â¤Î¡ÊÎ㤨¤Ð¡ÖWeb¥¢¥×¥ê¥±¡¼¥·¥ç¥ó¡×¤È¤«¡ÖJava¤Î¥»¥¥å¥ê¥Æ¥£µ¡¹½¡×¤È¤«¡Ë¤ÎÆÃħ¤ò¤¦¤Þ¤¯É½¤·¤Æ¤¤¤Æ¤«¤Ä¼«Æ°Åª¤Ê²òÀϤ¬²Äǽ¤ÊÌÏ·¿¤ò¡¤Í¸Â¥ª¡¼¥È¥Þ¥È¥óÅù¡¤·×»»¥â¥Ç¥ë¤È¸Æ¤Ð¤ì¤ë¤â¤Î¤òÁȤ߹ç¤ï¤»¤¿¤êÊÑ·Á¤·¤¿¤ê¤·¤Æ¹½ÃÛ¤¹¤ë¤³¤È¤¬¡¤¸¦µæ¤Î¼ç¤ÊÆâÍƤˤʤê¤Þ¤¹¡¥
¤Û¤«¤Ë¤â¡¤¥â¥Ç¥ë¸¡ºº¤ò¤â¤Ã¤È¼ê·Ú¤ËÍøÍѤǤ¤ë»ÅÁȤߤγ«È¯¤ä¡¤»ÅÍÍÄ̤꤫Ĵ¤Ù¤ë¤À¤±¤Ç¤Ê¤¯¡¤»ÅÍͤ˹礦¤è¤¦¤Ë¥×¥í¥°¥é¥à¤ò¼«Æ°Êѹ¹¤¹¤ë¸¦µæ¤Ê¤É¤Ë¤â¶½Ì£¤¬¤¢¤ê¤Þ¤¹¡¥
**¥â¥Ç¥ë¸¡ºº°Ê³°¤Î¸¡¾ÚË¡ [#o64c48ab]
''¸¡¾Ú''(verification)¡Ê¤Þ¤¿¤Ï·Á¼°Åª¸¡¾Ú(formal verification)¡Ë¤È¤Ï¡¤¿ôÍýŪ¤ÊÊýË¡¤ò»È¤Ã¤Æ¡Ö¥×¥í¥°¥é¥à¤¬´üÂÔÄ̤ê¤ÎÆ°ºî¤ò¤¹¤ë¡×¤³¤È¤òÊݾڤ¹¤ë¤³¤È¤Ç¤¹¡¥Â礤¯Ê¬¤±¤Æ¡¤''ÄêÍý¾ÚÌÀ''·¿¤Î¸¡¾Ú¤È''¥â¥Ç¥ë¸¡ºº''·¿¤Î¸¡¾Ú¤¬¤¢¤ê¤Þ¤¹¡¥
**ÄêÍý¾ÚÌÀ·¿¸¡¾Ú [#l21df926]
ÄêÍý¾ÚÌÀ·¿¤Î¸¡¾Ú¤È¤Ï¡¤Ê¸»úÄ̤ê¡Ö¥×¥í¥°¥é¥à¤¬´üÂÔÄ̤ê¤ÎÆ°ºî¤ò¤¹¤ë¡×¤³¤È¤Î''¾ÚÌÀ''¤òµ½Ò¤¹¤ë¡Ê¤¢¤ë¤¤¤ÏÀ¸À®¤¹¤ë¡Ë¤È¤¤¤¦ÊýË¡¤Ç¤¹¡¥
¤³¤³¤Ç¸À¤¦¾ÚÌÀ¤È¤Ï¡¤¥¢¥ë¥´¥ê¥º¥à¤ÎÀµÅöÀ¤Î¾ÚÌÀ¤ÈƱ¤¸¤¯¡¤
>- ¼Â¹Ô³«»Ï»þ¤Ë¤³¤¦¤¤¤¦À¼Á¤¬À®¤êΩ¤Ã¤Æ¤¤¤ë¡¥
>- ½¾¤Ã¤Æ1ʸÌܤÎľ¸å¤Ï¤³¤¦¤¤¤¦À¼Á¤¬À®¤êΩ¤Ã¤Æ¤¤¤ë¡¥
>- ½¾¤Ã¤Æ2ʸÌܤÎľ¸å¤Ï¤³¤¦¤¤¤¦À¼Á¤¬À®¤êΩ¤Ã¤Æ¤¤¤ë¡¥
>- ¡Ä
>- ½¾¤Ã¤ÆºÇ½ªÊ¸¤Îľ¸å¤Ï¤³¤¦¤¤¤¦À¼Á¤¬À®¤êΩ¤Ã¤Æ¤¤¤ë¡¥
¤È¤¤¤¦·Á¼°¤Ç¡¤ºÇ½ªÊ¸¤Î¼Â¹Ô¸å¤Ë¡Ö¥×¥í¥°¥é¥à¤Ë´üÂÔ¤µ¤ì¤ëÆ°ºî·ë²Ì¡×¤¬À®¤êΩ¤Ã¤Æ¤¤¤ë¤³¤È¤ò¼¨¤¹¤â¤Î¤Ç¤¹¡¥
¤¿¤À¤·¡¤¥ë¡¼¥×¤Î¤¢¤ë¥×¥í¥°¥é¥à¤Ç¤Ï¤â¤¦¾¯¤·¤ä¤ä¤³¤·¤¯¡¤¿ô³ØŪµ¢Ç¼Ë¡¤Î¤è¤¦¤Ë¡Ön²óÌܤ竤êÊÖ¤·¼Â¹Ô¸å¤ËÀ¼Á P ¤¬À®¤êΩ¤Ã¤Æ¤¤¤ì¤Ð¡¤(n+1)²óÌܤμ¹Ըå¤Ë¤â P ¤¬À®¤êΩ¤Ä¡×¤È¤¤¤¦¤è¤¦¤Ê·Á¼°¤Ç¾ÚÌÀ¤¹¤ëɬÍפ¬¤¢¤ê¤Þ¤¹¡Ê¤³¤Î¤è¤¦¤ÊÀ¼Á P ¤ò''¥ë¡¼¥×ÉÔÊѼ°''(loop invariant)¤È¸À¤¤¤Þ¤¹¡Ë¡¥
#br
¤³¤³¤Þ¤Çʹ¤¯¤È¡¤ÅöÁ³°Ê²¼¤Î¤è¤¦¤Êµ¿Ì䤬¤ï¤¯¤È»×¤¤¤Þ¤¹¡¥
+¤½¤Î¤è¤¦¤Ê¾ÚÌÀ¤ò¼ÂºÝ¤Ë¹Ô¤¦¤Î¤ÏÆñ¤·¤¹¤®¤ë¤Î¤Ç¤Ï?
+µ½Ò¤·¤¿¾ÚÌÀ¤Ë¸í¤ê¤¬¤Ê¤¤¤«¤É¤¦¤«¤Ï¤É¤¦³Îǧ¤¹¤ë¤Î¤«?
Àè¤Ë¸å¼Ô¤Ë¤Ä¤¤¤Æ½Ò¤Ù¤ë¤È¡¤¾ÚÌÀ¤òºîÀ®¤¹¤ë¤³¤È¤ÏÆñ¤·¤¯¤Æ¤â¡¤µ½Ò¤µ¤ì¤¿¾ÚÌÀ¤¬Àµ¤·¤¤¡Ê¤Ä¤Þ¤ê¾ÚÌÀ¤Î³Æ¥¹¥Æ¥Ã¥×¤ËÈôÌö¤¬¤Ê¤¤¡Ë¤«¤É¤¦¤«³Îǧ¤¹¤ë¤Î¤ÏÈæ³ÓŪ´Êñ¤Ç¡¤¤·¤«¤âµ¡³£Åª¤Ë¹Ô¤¨¤Þ¤¹¡¥¼ÂºÝ¡¤¤¢¤ë·è¤Þ¤Ã¤¿µ½Ò¸À¸ì¤Ç¾ÚÌÀ¤ò½ñ¤±¤Ð¡¤¤½¤ì¤¬Àµ¤·¤¤¤«¤É¤¦¤«¤ÏÄêÍý¾ÚÌÀ´ï¤È¸Æ¤Ð¤ì¤ë¥½¥Õ¥È¥¦¥§¥¢¥Ä¡¼¥ë¤ÇÄ´¤Ù¤ë¤³¤È¤¬¤Ç¤¤Þ¤¹¡¥
Á°¼Ô¤Îµ¿Ìä¤Ë¤Ä¤¤¤Æ¤Ï¡¤¼ÂºÝ¤Ë¤Ï¾ÚÌÀ¤ò´°Á´¤Ëµ½Ò¤·¤Ê¤¯¤Æ¤â¡¤¡ÖºÇ½é¤ËÀ®¤êΩ¤Ã¤Æ¤¤¤ëÀ¼Á¡Ê»öÁ°¾ò·ï¡Ë¡×¡ÖºÇ½ªÅª¤ËÀ®¤êΩ¤Ã¤Æ¤Û¤·¤¤À¼Á¡Ê»ö¸å¾ò·ï¡Ë¡×¡Ö¥ë¡¼¥×ÉÔÊѼ°¡×¤Ê¤É¡¤¾ÚÌÀ¤Î°ìÉôʬ¤Î¤ßµ½Ò¤¹¤ì¤Ð¡¤¤¢¤È¤ÏÄêÍý¾ÚÌÀ¥Ä¡¼¥ë¤¬ÅÓÃæ¤òÊä´°¤·¤Æ¤¯¤ì¤Þ¤¹¡Ê¤¿¤À¤·¡¤ÄêÍý¾ÚÌÀ¥Ä¡¼¥ë¤ÎǽÎϤˤϸ³¦¤¬¤¢¤ë¤Î¤Ç¡¤¥ë¡¼¥×ÉÔÊѼ°¤ä¤½¤Î¾¤ÎÊäÂê¤ò½½Ê¬Í¿¤¨¤Ê¤¤¤È¾ÚÌÀ¤Ë¼ºÇÔ¤·¤Þ¤¹¡Ë¡¥
***Îã [#afa1ffa1]
²¼¿Þ¤Ï¡¤¥½¥Õ¥È¥¦¥§¥¢¸¡¾Ú»Ù±ç´Ä¶ [[Why:http://why.lri.fr/]] ¤Î¥Þ¥Ë¥å¥¢¥ë¤Ëµ½Ò¤µ¤ì¤Æ¤¤¤ë¥×¥í¥°¥é¥àÎã¤Ç¤¹¡¥/*@ ¡Ä @*/ ¤È¤¤¤¦Éôʬ¤¬¡¤[[Java Modeling Language (JML):http://www.eecs.ucf.edu/~leavens/JML/]]¤È¤¤¤¦¸À¸ì¤Çµ½Ò¤µ¤ì¤¿»öÁ°¾ò·ï(requires)¡¤»ö¸å¾ò·ï(ensures)¡¤¥ë¡¼¥×ÉÔÊѼ°(loop-invariant)¡¤¤½¤Î¾¤ÎÊäÂê(lemma)¤Ç¤¹¡¥
#ref(Lesson1.java.png)
¤³¤³¤Ç¾ÚÌÀ¤·¤¿¤¤¤³¤È¤Ï¡¤´Ø¿ôsqrt¤ÎÌá¤êÃÍ(\result)¤Ë´Ø¤·¤Æ»ö¸å¾ò·ï¤¬À®¤êΩ¤Ä¤³¤È¡¤¤Ä¤Þ¤ê¡Ösqrt¤ÎÌá¤êÃͤϰú¿ô x ¤ÎÀµ¤ÎÊ¿Êýº¬¡Ê¤ÎÀ°¿ô¶á»÷¡Ë¤Ç¤¢¤ë¤³¤È¡×¤Ç¤¹¡¥¤·¤«¤·¡¤¤³¤ÎÎã¤Î»öÁ°¾ò·ï¤È»ö¸å¾ò·ï¤À¤±¤Ç¾ÚÌÀ¤ò¹Ô¤¦¤Î¤ÏÄêÍý¾ÚÌÀ¥Ä¡¼¥ë¤ÎǽÎϤòĶ¤¨¤Æ¤¤¤ë¤Î¤Ç¡¤Å¬Àڤʥ롼¥×ÉÔÊѼ°¤âÍ¿¤¨¤ëɬÍפ¬¤¢¤ê¤Þ¤¹¡¥¤Þ¤¿¡¤¤³¤ÎÎã¤Ç¤Ï¡¤²Ã»»¤È¾è»»¤ÎʬÇÛ§¤òÊÌÅÓÊäÂê¤È¤·¤ÆÍ¿¤¨¤ëɬÍפ¬¤¢¤ê¤Þ¤¹¡Ê¤É¤Î¤è¤¦¤Ê¥ë¡¼¥×ÉÔÊѼ°¤äÊäÂê¤òµ½Ò¤¹¤ì¤Ð¤è¤¤¤«¤Ï¡¤¤¢¤ëÄøÅÙ»î¹Ôºø¸í¤·¤Æ¸«¤Ä¤±¤ëɬÍפ¬¤¢¤ê¤Þ¤¹¡Ë¡¥
¤³¤Î¤è¤¦¤Êµ½Ò¤ò²Ã¤¨¤¿¥×¥í¥°¥é¥à¤ò Why ¤ËÆþÎϤ¹¤ë¤È¡¤¤¢¤È¤Ï¼«Æ°Åª¤Ë»ö¸å¾ò·ï¤¬À®¤êΩ¤Ã¤Æ¤¤¤ë¤³¤È¤ò¾ÚÌÀ¤·¤Æ¤¯¤ì¤Þ¤¹¡Ê²¼¿Þ¡Ë¡¥¿Þ¤Î±¦¾åÉô¤ÎÎΰè¤Ëɽ¼¨¤µ¤ì¤Æ¤¤¤ë¤Î¤¬¡¤¤½¤Î²¼¤ÎÎΰè¤Ë¥ª¥ì¥ó¥¸¿§¤Ç¼¨¤µ¤ì¤Æ¤¤¤ë¼°¡Ê»ö¸å¾ò·ï¤Î°ìÉô¡Ë¤ËÂФ·¤ÆÄêÍý¾ÚÌÀ¥Ä¡¼¥ë¤¬ºîÀ®¤·¤¿¡Ö¾ÚÌÀ¡×¤Ç¤¹¡¥
#ref(gwhy-Lesson1.png)
**¥â¥Ç¥ë¸¡ºº ºÆˬ [#re95b2f3]
''¥â¥Ç¥ë¸¡ºº''(model-checking)¤È¤Ï¡¤¸¡ººÂоݤǤ¢¤ë¥·¥¹¥Æ¥à¤ò͸¥ª¡¼¥È¥Þ¥È¥ó¡Ê¤Þ¤¿¤Ï¤½¤Î³ÈÄ¥¡Ë¤Ë¶á»÷¤·¡¤²Äǽ¤Ê¼Â¹Ô·ÐÏ©¤òÌÖÍåŪ¤ËÄ´¤Ù¤ë¤³¤È¤Ç¡¤¡Ö˾¤Þ¤·¤¯¤Ê¤¤¾õÂ֡ʥǥåɥí¥Ã¥¯¤Ê¤É¡Ë¤Ë´Ù¤é¤Ê¤¤¤«¡×¤ä¡ÖÌÜŪ¤Î¾õÂÖ¤ËÅþ㤹¤ë¤³¤È¤¬²Äǽ¤«¡×Åù¤òÄ´¤Ù¤ëÊýË¡¤Ç¤¹¡Ê¶á»÷¤ÇÆÀ¤é¤ì¤¿Í¸Â¥ª¡¼¥È¥Þ¥È¥ó¤ò¸¡ººÂоݤÎ''¥â¥Ç¥ë''¤È¸À¤¤¤Þ¤¹¡Ë¡¥
ÄêÍý¾ÚÌÀ·¿¸¡¾Ú¤ËÈæ¤Ù¤Æ¸¡¾Ú¤Ç¤¤ëÀ¼Á¤¬¸ÂÄꤵ¤ì¤Þ¤¹¤¬¡¤ÄêÍý¾ÚÌÀ·¿¸¡¾Ú¤Ç¤Ï¿Í´Ö¤¬¥ë¡¼¥×ÉÔÊѼ°¤äÊäÂê¤ò¤è¤¯¹Í¤¨¤Æµ½Ò¤·¤Ê¤±¤ì¤Ð¤¤¤±¤Ê¤¤¤Î¤ËÂФ·¡¤¥â¥Ç¥ë¸¡ºº¤Ç¤ÏºÇ½ªÅª¤ËËþ¤¿¤·¤Æ¤Û¤·¤¤À¼Á¤Î¤ßµ½Ò¤¹¤ë¤À¤±¤Ç¸¡¾Ú¤¬¹Ô¤¨¤Þ¤¹¡¥Ê¹ԥ·¥¹¥Æ¥à¤äÄÌ¿®¥×¥í¥È¥³¥ë¤Ê¤É¡¤¥â¥¸¥å¡¼¥ë´Ö¤ÎÆ°ºî¥¿¥¤¥ß¥ó¥°¤¬½ÅÍפʥ·¥¹¥Æ¥à¤Î¸¡¾Ú¤Ë¤ÏÆä˸þ¤¤¤Æ¤¤¤Þ¤¹¡¥
͸¥ª¡¼¥È¥Þ¥È¥ó¤Ø¤Î¥â¥Ç¥ë²½¤ä¡¤¸¡¾Ú¤·¤¿¤¤À¼Á¤Îµ½Ò¤Ë¤Ï¡¤¤¢¤ëÄøÅÙ¤ÎÃ챤¬É¬ÍפǤ¹¡¥Ä̾¸¡ººÂоݥ½¥Õ¥È¥¦¥§¥¢¤ÎÆ°ºî¤ò´°Á´¤Ëɽ¸½¤·¤¿Í¸Â¥ª¡¼¥È¥Þ¥È¥ó¤Ç¤Ï¡¤¾õÂÖ¿ô¤¬ÇüÂç¤Ë¤Ê¤ê¡¤¸½¼ÂŪ¤Ê»þ´Ö¤Ç¤Ï¸¡¾Ú¤¬¤Ç¤¤Þ¤»¤ó¡¥¼ê¤ËÉ館¤ëÂ礤µ¤Ë¶á»÷¤·¤Ê¤¤¤È¤¤¤±¤Þ¤»¤ó¤¬¡¤ËÜÍè¤Î¸¡ººÂоݤȤκ¹¤¬Â礤¯¤Ê¤ê²á¤®¤ë¤È¸¡¾Ú¤¬Ìµ°ÕÌ£¤Ë¤Ê¤Ã¤Æ¤·¤Þ¤¦¤È¤¤¤¦ÌäÂ꤬¤¢¤ê¤Þ¤¹¡¥
*** Êä»ñÎÁ [#ie021e60]
-[[2012ǯÅÙ±þÍÑ¥½¥Õ¥È¥¦¥§¥¢¹©³ØÏÀ>Lecture/AdvancedSE]]
--¥â¥Ç¥ë¸¡ºº¤Ë´Ø¤¹¤ë²áµî¤Î¼ø¶È¤Î»ñÎÁ¡£
***Îã [#lc389ead]
²¼¿Þ¤Ï¡¤¥â¥Ç¥ë¸¡ºº»Ù±ç´Ä¶ [[Uppaal:http://www.uppaal.com/]] ¤ò»È¤Ã¤Æ¡¤Èó¾ï¤Ë´Êñ¤Ê¥¨¥ì¥Ù¡¼¥¿¥·¥¹¥Æ¥à¤Î¸¡¾Ú¤ò¹Ô¤ª¤¦¤È¤·¤Æ¤¤¤ëÎã¤Ç¤¹¡¥¤³¤Î¥·¥¹¥Æ¥à¤Ï¡¤1¡Á3³¬¤ò°ÜÆ°¤¹¤ë¥«¥´¤È¡¤³Æ³¬¤Î¸Æ¤Ó½Ð¤·¥Ü¥¿¥ó¤«¤é¹½À®¤µ¤ì¡¤¤½¤ì¤¾¤ì¤ÎÆ°ºî¤¬Í¸Â¥ª¡¼¥È¥Þ¥È¥ó¤Çµ½Ò¤µ¤ì¤Æ¤¤¤Þ¤¹¡ÊÄ̾ï¤Î°ÕÌ£¤Î͸¥ª¡¼¥È¥Þ¥È¥ó¤è¤ê¤Ï³ÈÄ¥¤µ¤ì¤Æ¤¤¤Æ¡¤floor¤äarrive¤È¤¤¤Ã¤¿ÊÑ¿ô¤¬¼è¤êÉÕ¤±¤é¤ì¡¤ÊÑ¿ô¤ÎÃͤˤè¤Ã¤Æ¾õÂÖÁ«°Ü¤¬²Äǽ¤«¤É¤¦¤«ÊѤï¤ê¤Þ¤¹¡Ë¡¥
#ref(Uppaal-1.png)
²¼¿Þ¤Ç¤Ï¡¤¤³¤Î¥¨¥ì¥Ù¡¼¥¿¥·¥¹¥Æ¥à¤ËÂФ·¡¤¡Ö1³¬¤Î¸Æ½Ð¥Ü¥¿¥ó¤¬²¡¤µ¤ì¤¿¤é¡¤¤¤¤Ä¤«¤Ï1³¬¤ËÃ夯¡×Åù¤ÎÀ¼Á¤¬À®¤êΩ¤Ä¤«¤É¤¦¤«¸¡¾Ú¤·¤Æ¤¤¤Þ¤¹¡¥¸¡¾Ú¤·¤¿¤¤À¼Á¤Ï''»þÁêÏÀÍý''(temporal logic)''¼°''¤È¤¤¤¦ÆÈÆäεˡ¤Çµ½Ò¤·¤Þ¤¹¡¥¤³¤ÎÎã¤Ç¤Ï¡Ö1³¬¤Î¸Æ½Ð¥Ü¥¿¥ó¤¬²¡¤µ¤ì¤¿¤é¡¤¤¤¤Ä¤«¤Ï1³¬¤ËÃ夯¡×¤È¤¤¤¦À¼Á¤ÏÀ®¤êΩ¤¿¤º¡¤ÀÖ¿§¤Î°õ¤Ç¤½¤Î¤³¤È¤¬¼¨¤µ¤ì¤Æ¤¤¤Þ¤¹¡¥
#ref(Uppaal-2.png)
À¼Á¤¬À®¤êΩ¤¿¤Ê¤¤¾ì¹ç¡¤¤½¤ì¤¬¤É¤Î¤è¤¦¤ÊÆ°ºî½ç½ø¤ò¤¿¤É¤Ã¤¿¤È¤¤Ëµ¯¤³¤ë¤«¡Ê¤³¤ÎÆ°ºî½ç½ø¤ò''È¿Îã''¤È¸À¤¤¤Þ¤¹¡Ë¤òÊ̤βèÌ̤dzÎǧ¤Ç¤¤ë¤Î¤Ç¡¤¤½¤ì¤ò¸«¤Æ¥·¥¹¥Æ¥à¤ò½¤Àµ¤¹¤ë¤³¤È¤Ë¤Ê¤ê¤Þ¤¹¡¥
#br
¡Ê¤Á¤Ê¤ß¤Ë¾åµ¤Î¥·¥¹¥Æ¥à¥â¥Ç¥ë¤Ç¤Ï¤Ê¤¼¤³¤ÎÀ¼Á¤òËþ¤¿¤µ¤Ê¤¤¤«¤È¤¤¤¦¤È¡¤¾åµ¤Î¥â¥Ç¥ë¤Ç¤Ï¡Ö¥«¥´¤¬2³¬¤Ë¤¢¤ë¤È¤¤Ë1³¬¤«¤é¤â3³¬¤«¤é¤â¸Æ¤Ó½Ð¤µ¤ì¤Æ¤¤¤ë¾ì¹ç¡¤¥«¥´¤Ï¤É¤Á¤é¤Ç¤â¹¥¤¤ÊÊý¤Ë¸þ¤«¤Ã¤Æ°ÜÆ°¤Ç¤¤ë¡×¤«¤é¤Ç¤¹¡¥½¾¤Ã¤Æ¡¤°Ê²¼¤ÎÆ°ºî½ç½ø¤ò¤¿¤É¤ë¤È¡Ö1³¬¤Î¥Ü¥¿¥ó¤¬²¡¤µ¤ì¤Æ¤¤¤ë¤Î¤Ë¤¤¤Ä¤Þ¤Ç¤â1³¬¤Ë¤Ï¥«¥´¤¬Ã夫¤Ê¤¤¡×¤³¤È¤¬µ¯¤³¤ê¤Þ¤¹¡Ê¤³¤Î¤è¤¦¤ÊÆ°ºî½ç½ø¤¬¡ÖÈ¿Îã¡×¤Ç¤¹¡Ë¡¥
+3³¬¤Î¸Æ¤Ó½Ð¤·¥Ü¥¿¥ó¤¬²¡¤µ¤ì¤ë¡¥
+¥«¥´¤¬3³¬¤Ë¸þ¤«¤Ã¤Æ°ÜÆ°¤ò»Ï¤á¤ë¡¥
+1³¬¤Î¸Æ¤Ó½Ð¤·¥Ü¥¿¥ó¤¬²¡¤µ¤ì¤ë¡¥
+¥«¥´¤¬3³¬¤ËÃ夯¡¥
+¥«¥´¤¬1³¬¤Ë¸þ¤«¤Ã¤Æ°ÜÆ°¤ò»Ï¤á¤ë¡¥
+3³¬¤Î¸Æ¤Ó½Ð¤·¥Ü¥¿¥ó¤¬²¡¤µ¤ì¤ë¡¥
+¥«¥´¤¬2³¬¤ËÃ夯¡¥
+1³¬¤È3³¬¤Î¥Ü¥¿¥ó¤¬²¡¤µ¤ì¤Æ¤¤¤ë¤Î¤Ç¡¤¥«¥´¤Ï3³¬¤Ë¸þ¤«¤Ã¤Æ°ÜÆ°¤¹¤ë¡¥
+¾åµ4°Ê¹ß¤ò̵¸Â¤Ë·«¤êÊÖ¤¹¡¥
¤Ä¤Þ¤ê¡¤3³¬¤Ë¤Ò¤Ã¤¤ê¤Ê¤·¤Ë¤ªµÒ¤µ¤ó¤¬¤ä¤Ã¤Æ¤¤Æ¡¤¤«¤Ä¡¤¥¨¥ì¥Ù¡¼¥¿¥·¥¹¥Æ¥à¤¬1³¬¤ÇÂԤäƤ¤¤ë¤ªµÒ¤µ¤ó¤òÊü¤Ã¤Æ¤ª¤¤¤Æ3³¬¤Î¤ªµÒ¤µ¤ó¤ÎÊý¤Ë¤Ð¤«¤ê¸þ¤«¤¦¡¤¤È¤¤¤¦¾õ¶·¤ËÁêÅö¤·¤Þ¤¹¡¥
¤³¤ÎÉÔ¶ñ¹ç¤ò¼è¤ê½ü¤¯¤¿¤á¤Ë¤Ï¡¤Î㤨¤Ð¡Ê¸½¼Â¤Î¥¨¥ì¥Ù¡¼¥¿¤ÈƱÍͤˡˡ֥«¥´¤¬2³¬¤Ë¤¢¤ë¤È¤¤Ë1³¬¤«¤é¤â3³¬¤«¤é¤â¸Æ¤Ó½Ð¤µ¤ì¤Æ¤¤¤ë¾ì¹ç¡¤Ä¾Á°¤Î°ÜÆ°Êý¸þ¡Ê¾å¾º¤Þ¤¿¤Ï²¼¹ß¡Ë¤ò°Ý»ý¤¹¤ë¡×¤è¤¦¤Ë¥·¥¹¥Æ¥à¤ò½¤Àµ¤·¤Þ¤¹¡¥¡Ë