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 н α׷