Ʈ Ư (1б)
- Introduction to Formal Methods ( )      


(2009 Spring for graduate students in HONGIK University)

Text :
   - System and Software Verification : Model Checking Techniques and Tools (Springer, 1999)

Schedule

WEEKS DATE Course
1 04.10 14:00  Introduction to Formal Specification (paper)
 Formal Modeling and Verification of Safety-Critical Software 
2 04.17 10:00  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
 Chapter 11. Abstraction Methods
 Chapter 12. SMV
 Chapter 13. SPIN
 Chapter 14. DESIGN/CPN
 Chapter 15. UPPAAL
 Chapter 16. KRONOS
 Chapter 17. HYTECH

 ȫʹ SE Lab. Ȱ Ұ
    - ȼ(2)
    - (1)/쿭(4)
    - 赿ȣ(4)

3 04.24 10:00
4 05.08 10:00
5 05:09 10:00
6 05.16 10:00
7 05.22 09:00
8 05.29 14:00
9 06.05 10:00
10 06.12 10:00
11 06.19 10:00
12
13
14
15
16

Ʈ (2б)

Objective :
  
- ̻ ϼմϴ.

Overview :
   - DZб õ 1207ȣ ǽǿ մϴ.
   - 14:00 ~ 17:00
   - ȭǥ 2ð

Schedule

WEEKS DATE Course
1 09.04  ް. (RE'09 )
2 09.11  Introduction
3 09.18  쿭(2) , ȼ()
4 09.25  赿ȣ()
5 10.02  ް. (߼)
6 10.09  ع
7 10.16  ()
8 10.23  쿭(1, 1)
9 10.30  (߰) , ȼ(߰)
10 11.06  赿ȣ(߰) , 쿭(߰)
11 11.13  ع
12 11.20  ȼ()
13 11.27  쿭()
14 12.04  ް. (ȥ)
15 12.11  ް. (ȥ)
16 12.18  赿ȣ (߰), ()
01.11  쿭 2 ()
01.18  赿ȣ() , () , ȼ()