°í±Þ¼ÒÇÁÆ®¿þ¾î°øÇÐ
   - Introduction to Model Checking  (2026 Spring)

¡¡

Course Syllabus

¡¡

2026.03.05 : 2026³â 1Çб⠰ú¸ñ ȨÆäÀÌÁö °³¼³ÇÕ´Ï´Ù.
                + À̹ø Çб⿡´Â ÀüÅëÀûÀÎ Á¤Çü±â¹ý (Formal Method)À» °øºÎÇÏ°í Á÷Á¢ È°¿ëÇؼ­ ¿¬±¸³í¹®À» ÀÛ¼ºÇÏ´Â °ÍÀ» ¸ñÇ¥·Î ÇÕ´Ï´Ù.
                + °­»ç°¡ ³ìÈ­ÇÑ KCOW µ¿¿µ»ó °­ÀǸ¦ ÀϺΠȰ¿ëÇÕ´Ï´Ù.
¡¡

Schedule

Week Date ±Ý¿äÀÏ - ½Å°øÇаü 1010È£ (12:00~15:00)
1 03.09

   Course Introduction (Lecture Note)
    
   Chapter 1. Automata  (KOCW)
   Chapter 2. Temporal Logic  (KOCW)
   Chapter 3. Model Checking  (KOCW)
   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 

   Statecharts
   NuSMV
   VIS
   UPPAAL
   SPIN
   Petri Net

   KOCW °­ÀÇ ¸µÅ© :  http://www.kocw.or.kr/home/cview.do?cid=ce3fa349e18d7875
2 03.16
3 03.23
4 03.30 (¹ßÇ¥#1)
5 04.06 (¹ßÇ¥#2)
6 04.13
7 04.20 (Áß°£°í»ç)
8 04.27
9 05.04 (¹ßÇ¥#3)
10 05.11 (¹ßÇ¥#4)
11 05.18 (ÈÞ°­)
12 05.25 (°øÈÞÀÏ)
13 06.01
14 06.08 (¹ßÇ¥#5)
15 06.15 (±â¸»°í»ç)
16 06.22 (Reserved)


ÆÀ¸í ÆÀ¿ø ¿¬±¸³í¹®¿¡
»ç¿ëÇÑ ¸ðµ¨Ã¼Ä¿		 ÆÀ¹ßÇ¥ #1 ÆÀ¹ßÇ¥ #2 ÆÀ¹ßÇ¥ #3 ÆÀ¹ßÇ¥ #4 ÆÀ¹ßÇ¥ #5
ÀÚÆDZâ
(NuSMV 1Â÷)

ÀÚÆDZâ
(NuSMV 2Â÷)

 ¼±ÅÃÇÑ
µµ±¸ ¹ßÇ¥		 ÀÚÆDZâ
(¼±ÅÃÇÑ µµ±¸·Î)		 ¿¬±¸³í¹® ¹ßÇ¥
T1 ¡¡

Statechart

 ¡¡ ¡¡ ¡¡ ¡¡ ¡¡
T2 ¡¡ SPIN ¡¡ ¡¡ ¡¡ ¡¡ ¡¡
T3 ¡¡ VIS ¡¡ ¡¡ ¡¡ ¡¡ ¡¡
T4 ÀÌ¿µ±Ô, ÇãÀ±¾Æ SPIN, UPPAAL ¹ßÇ¥ÀÚ·á, ¼Ò½ºÄÚµå ¡¡ ¡¡ ¡¡ ¡¡