Advanced Software Engineering ( Ʈ)
 - Introduction to Model Checking Theories and Tools  
(2014 Fall for graduate students)

Course Syllabus

Schedule

Week Date Lecture Projects & Presentations
1 09.05    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 

 10.03 : õ
 
 11.14 : ߰

 12.12 : ް (ISIC 2014 )

 12.19 : ⸻ 

2 09.12
3 09.19
4 09.26
5 10.03
6 10.10
7 10.17
8 10.24
9 10.31
10 11.07
11 11.14
12 11.21
13 11.28
14 12.05
15 12.12
16 12.19

Team Projects

1 ǥ (09.26)
- Introduction
2 ǥ (10.10)
- Dining Philosophers
3 ǥ (10.31)
- Dining Philosophers
4 ǥ (11.21)
- GetOut (SMV)
5 ǥ (11.28)
- GetOut (SPIN)
6 ǥ (12.05)
-
7 ǥ (12.19)
- ǥ
TIMES Ұ - - - -
翱 , Cadence SMV Ұ DP (w SMV) DP DP2 (w SPIN) GO GO
, Ӵ㼷 SPIN Ұ DP (w SPIN) DP (w SMV) GO Simple WAN Fabrics
, ѱȫ SPIN Ұ DP (w SPIN) DP (w SMV) GO
ڼ , NuSMV Ұ DP (w SMV) DP (w SPIN) GO GO κü Interrupt 帧