¼ÒÇÁÆ®¿þ¾î ÃøÁ¤ Ư·Ð (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. ¿¬±¸È°µ¿ ¼Ò°³ ¹× ÇâÈÄ ¿¬±¸¹æÇâ °øÀ¯ |
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 :
- °Ç±¹´ëÇб³ »õõ³â°ü 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 | ±èµ¿È£(¸¶¹«¸®) , ¼ÕÇö½Â(¸¶¹«¸®) , ¾È¼ººó(¸¶¹«¸®) |
¡¡
¡¡
¡¡