Advanced Software Engineering ( Ʈ)
- Introduction to Formal Methods      

(2011 Fall for graduate students)

Course Syllabus


2011.08.29 :  09.09 ʹ 10:00 մϴ.    
2011.09.10 :  T5 ʹ 09.23 Ŀ ǥմϴ. T1 ~ T4 09.16 ǥϽø ǰڽϴ.
                - ǥ 20 ܷ Ź 帳ϴ. 
                - ǥڷ ǥ 09:00 pdf ֽø Ȩ ε ϰڽϴ.            
2011.09.15 :  ǥ Ͻô Ʒ ̺ Ȯϼ.
2011.10.26 :  10.28 Ʒ ۷ üմϴ. 09:10 1 Ұ ּ.
                UBITA 2011 ƽþ ۷ (α׷, )
2011.11.03 :  ߰ 11.11 ڽϴ.
                ߰ Case Study ǥ 11.18 մϴ. (11.18: T1~T6, 11.25: T7 ~)


Schedule

Week Date Lecture Etc.
1 09.02
   Course Introduction (Lecture Note)
   Introduction to Formal Methods (paper, ppt)
 
   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 
2 09.09
3 09.16 ߼ (09.12~13) / ǥ #1 : Ұ
4 09.23 ǥ #1 : Ұ
5 09.30
6 10.07
7 10.14
8 10.21
9 10.28
10 11.04
11 11.11 ߰ (11.11)
12 11.18  ǥ #2 : Case Study (11.18 ~)
13 11.25
14 12.02 ǥ #3 : Proposal
15 12.09
16 12.16


Term Projects

- :

    - /

    - Ұ

    - ϳ Ͽ, Full Case Study

    - ̸ Ȱ

- :

A. SMV

B. SPIN

C. VIS

D.  UPPAAL

E. SAT Solver

F. CBMC (HW-CBMC)

G. BLAST

H. SCADE

I. HyTech

J. TIMES

K. SpaceEx

Ұ Case Study ǥ
T1 HyTech (09.16) Car Collision ǥ
T2 (û) SMT Solver (09.16) -
T3 ۽ȭ TIMES  (09.16) OFP μ 층 м ǥ (w )
T4 UPPAAL  (09.23) Smartphone controller for UAVs ǥ
T5 , ֽ CBMC (09.23) ARIS ȣȭ ˰ ǥ
T6 ̵(û) , TIMES (09.23) -
T7 () SPIN (09.30) -
T8 ̿ SPIN (09.30) Cooperative Communication ǥ
T9 SMV (09.30) ȭ簨 ǥ
T10 Ѽ CBMC (09.30) ǥ
T11 δ پ SCADE (09.30) װ Ʈѷ 𵨸 ǥ,1,2,3