Advanced Software Engineering (°í±Þ ¼ÒÇÁÆ®¿þ¾î°øÇÐ)
 - Introduction to Model Checking Theories and Tools  
(2015 Spring for graduate students)
¡¡

Course Syllabus
¡¡

+ ³í¹® ¾²±â·Î ÇÑ ÆÀÀº, ³í¹® Á¦Ãâ ¿Ï·á ½Ã A+ ÇÐÁ¡ ³ª°©´Ï´Ù. (~06.24)
+ ºñ³í¹® Á¦Ãâ ÆÀÀÇ ÃÖ°í ÇÐÁ¡Àº A
+ ¸ðµ¨¸µ/°ËÁõÀ» ¼öÇ൵ ¸ø ÇØ º» ÆÀÀº B+ ÀÌ ÃÖ°í ÇÐÁ¡ÀÔ´Ï´Ù.

¡¡

Schedule

Week Date Lecture Projects & Presentations
1 03.02    Course Introduction (Lecture Note)
    
   Chapter 1. Automata
   Chapter 2. Temporal Logic
   Chapter 3. Model Checking
   Chapter 4. Symbolic Model Checking
   Chapter 5. Timed Automata
   Chapter 6. Reachability Properties
   Chapter 7. Safety Properties
   Chapter 8. Liveness Properties
   Chapter 9. Deadlock-freeness
   Chapter 10. Fairness Properties 

 04.20 - Áß°£°í»ç

 05.25 - °øÈÞÀÏ

 06.15 - ±â¸»°í»ç

2 03.09
3 03.16
4 03.23
5 03.30
6 04.06
7 04.13
8 04.20
9 04.27
10 05.04
11 05.11
12 05.18
13 05.25
14 06.01
15 06.08
16 06.15

¡¡

Team Projects

ÆÀ 1Â÷ ¹ßÇ¥
Introduction
(SMV , SPIN)
ÄûÁî
(C ¾ð¾î)
2Â÷ ¹ßÇ¥
ÀÚÆDZâ (SMV)
3Â÷ ¹ßÇ¥
ÀÚÆDZâ (SMV2)
4Â÷ ¹ßÇ¥
ÀÚÆDZâ
(SPIN ½Ã¹ü)
5Â÷ ¹ßÇ¥
ÀÚÆDZâ (SPIN)
5.5Â÷ ¹ßÇ¥
ÀÚÆDZâ
(SPIN2)
6Â÷ ¹ßÇ¥
ÇÁ·ÎÆ÷Àý
7Â÷ ¹ßÇ¥
Áß°£¹ßÇ¥
ÃÖÁ¾¹ßÇ¥ ³í¹®
03.30 04.13 04.27 05.04 05.11 05.18 ¡¡ 06.01 06.08 06.15
ÁøÁ¤ÇÏ, ±è¿ìºó SMV   SMV SMV2   SPIN
SPIN2 ¡¡ÇÁ·ÎÆ÷Àý SPIN SPINÀ» È°¿ëÇÑ ´ÙÁß°æ·Î Ad-hoc
N/W ¶ó¿ìÆà ÇÁ·ÎÅäÄÝ Á¤Çü°ËÁõ + ³í¹®
¡¡
±è±×¸°, ±è¹Ù¿ï SPIN ¡¡ SMV SMV2 ¡¡ SPIN SPIN2 ±è¹Ù¿ï
±è±×¸°
±è¹Ù¿ï
±è±×¸°

ÀÚµ¿¼³Ä¡½Ã½ºÅÛÀÇ Host HW Á¤º¸ ¹× »ç¿ëÀÚ¼³Á¤ ±â¹Ý ¼³Ä¡ ½Å·Ú¼º¿¡ ´ëÇÑ Á¤Çü°ËÁõ (±è¹Ù¿ï)
+

SpinÀ» ÀÌ¿ëÇÑ »ç¹° ÀÎÅÍ³Ý È¯°æ¿¡¼­ °æ·®È­ ÀåÄ¡ °£ »óÈ£ ÀÎÁõÀÇ Ãë¾à¼º Á¤Çü °ËÁõ (±è±×¸°) + ³í¹®

¡¡
Çã¿õ, ±èÁØÅ SMV/SPIN   SMV SMV2   SPIN SPIN2 ÇÁ·ÎÆ÷Àý SPIN À¥ ºê¶ó¿ìÀú¿¡¼­ ·Î±×ÀÎ À¯Áö ¹× Cookie Hijacking ¹æÁö¸¦
À§ÇÑ Dynamic Cookie ±â¹ý °ËÁõ
¡¡
¹Ú½Â¼ö, ±è¿µ¼¼ SPIN   SMV SMV2   SPIN SPIN2 ÇÁ·ÎÆ÷Àý SPIN SPINÀ» ÀÌ¿ëÇÑ TCP/UDP ¹æ½ÄÀÇ RADIUS ÇÁ·ÎÅäÄÝ ½Å·Ú¼º ¹× ¼Óµµ ºñ±³ ¡¡
±èÁö¿ø, ¾È°æ¸ð SPIN   SMV SMV2   SPIN SPIN2   ÇÁ·ÎÆ÷Àý CBMC ¹®¼­ »çÀÌÀÇ À¯»ç¼ºÀ» °è»êÇÏ´Â Block SwapÀ» È°¿ëÇÑ ÆíÁý°Å¸® ¾Ë°í¸®ÁòÀÇ Á¤È®¼º Á¤Çü°ËÁõ ¡¡
¹ÚÀç¿î, À±¹ÎÁö SMV   SMV SMV2   SPIN SPIN2   ÇÁ·ÎÆ÷Àý SPIN M2Mȯ°æ¿¡¼­ µ¥ÀÌÅÍ󸮸¦ À§ÇÑ MinGJW¾Ë°í¸®Áò »ç¿ëÀÇ Á¤È®¼º °ËÁõ + ³í¹®1 ³í¹®2 ¡¡
Á¤ÇõÁØ, ±è¼º¹Î, ¼Û¿µ¼® SMV   SMV SMV2 SPIN -
Best Practice
  UPPAAL ÇÁ·ÎÆ÷Àý UPPAAL Formal Modeling and Verification of
Serial Communication in UAVs + ³í¹®(8Àå±îÁö)
¡¡
±èÅÂÇö SMV/SPIN   SMV SMV2 NuDE SPIN SPIN2   ÇÁ·ÎÆ÷Àý SMV ¿µ¾îÇнÀ ÇÁ·Î±×·¥ÀÇ Á¤Çü°ËÁõ ¡¡

¡¡