Advanced Software Engineering ( Ʈ)
- Introduction to Formal Methods      

(2009 Fall for graduate students)

Course Syllabus

2009.10.05 :  10.09() Ʒ ްմϴ.
2009.11.07 :  11.13() ߰ ϴ. ð: 09:00 ~ 10:00 , : 1,2,3,5
2009.11.07 :  Ʈ (2/1) Ϸ ˷ ּ. (~11.13)
2009.11.19 :  ߰ Ȯϼ.
                Ʈ ϼž մϴ.
                ⸻ Ʈ üϰڽϴ.
2009.11.25 :  12.04() 12.03() ϰڽϴ.
                : 904ȣ ع
                ð : 14:00 ~ 21:00 ƹ
                : UBS ǥڷ UPPAAL ͼ, 濡 ǥմϴ.
2009.12.18 :  ⼮ο Ǿϴ.
                ǥڷ ּ.
                б ϼ̽ϴ.
2009.12.21 :  Ȯϼ.
                ũ żϰ ּ.


Schedule

Week Date Lecture Etc.
1 09.04  ް (RE'09 )
2 09.11  Introduction to Formal Specification (Paper)
 Chapter 1. Automata
 Chapter 2. Temporal Logic
 Chapter 3. Model Checking
 Chapter 4. Symbolic Model Checking
 Chapter 5. Timed Automata
3 09.18
4 09.25
5 10.02  ް (߼)
6 10.09
7 10.16
8 10.23
9 10.30
10 11.6
11 11.13  ߰
12 11.20  Ʈ Ұ
   - UPPAAL

 
 氭(6~10)
   Chapter 6. Reachability Properties
   Chapter 7. Safety Properties
   Chapter 8. Liveness Properties
   Chapter 9. Deadlock-freeness
   Chapter 10. Fairness Properties

Ʈ : CVM
뵵: UPPAAL

(2/1)

13 11.27  ߰ǥ : I
14 12.04  ߰ǥ : II
15 12.11  ް
16 12.18  ǥ :


Team Project

Formal
Specification #1
Formal
Specification #2
Formal
Verification
T1 200871214   200874157 ؼ
200973354 ȣ
ؼ ȣ , CVM
T2 200971192 ̱ټ  200973344 ؿ ̱ټ ؿ ̱ټ , CVM
T3

200974155 ȣ  200974158 ּ
200871216
ö

ȣ ּ ö , CVM
T4 200973359   200973349 , CVM
T5 200973353   200973347
200973345
, CVM
T6 200973349 Ѹ  200973355 Ѹ Ѹ , CVM
T7 200973352 õ  200974157
200874158 ̹
̹ õ , CVM
T8 200974154 ö  200981021 - ö , CVM
T9 200981011   200973214 - , CVM