Advanced Software Engineering (°í±Þ ¼ÒÇÁÆ®¿þ¾î°øÇÐ)
- Introduction to Model Checking
Theories and Tools
(2014 Fall for graduate students)
¡¡
Schedule
| Week | Date | Lecture | Projects & Presentations |
| 1 | 09.05 | 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 |
10.03 : °³ÃµÀý |
| 2 | 09.12 | ||
| 3 | 09.19 | ||
| 4 | 09.26 | ||
| 5 | 10.03 | ||
| 6 | 10.10 | ||
| 7 | 10.17 | ||
| 8 | 10.24 | ||
| 9 | 10.31 | ||
| 10 | 11.07 | ||
| 11 | 11.14 | ||
| 12 | 11.21 | ||
| 13 | 11.28 | ||
| 14 | 12.05 | ||
| 15 | 12.12 | ||
| 16 | 12.19 |
¡¡
Team Projects
| ÆÀ | 1Â÷ ¹ßÇ¥ (09.26) - Introduction |
2Â÷ ¹ßÇ¥ (10.10) - Dining Philosophers |
3Â÷ ¹ßÇ¥ (10.31) - Dining Philosophers |
4Â÷ ¹ßÇ¥ (11.21) - GetOut (SMV) |
5Â÷ ¹ßÇ¥ (11.28) - GetOut (SPIN) |
6Â÷ ¹ßÇ¥ (12.05) - ÇÁ·ÎÆ÷Àý |
7Â÷ ¹ßÇ¥ (12.19) - ³í¹®¹ßÇ¥ |
| ¼¿µÁÖ | TIMES ¼Ò°³ | - | - | - | - | ¹ÌÁ¤ | Á¤¼¼Áø |
| ±èÀ翱 , Á¤¼¼Áø | Cadence SMV ¼Ò°³ | DP (w SMV) | DP DP2 (w SPIN) | GO | GO¡¡ | ||
| ¿ÀÁØ , ÀÓ´ã¼· | SPIN ¼Ò°³ | DP (w SPIN) | DP (w SMV) | GO | Simple WAN Fabrics¡¡ | ¿ÀÁØ | |
| ±è´ëÈñ , ÇѱâÈ« | SPIN ¼Ò°³ | DP (w SPIN) | DP (w SMV) | GO¡¡ | |||
| ¹Ú¼ºÈÆ , ¹ÚÁø¼º | NuSMV ¼Ò°³ | DP (w SMV) | DP (w SPIN) | GO | GO¡¡ | ¹«ÀκñÇàü Interrupt È帧Á¦¾î | ¹ÚÁø¼º |
¡¡
¡¡
