Advanced Software Engineering (°í±Þ ¼ÒÇÁÆ®¿þ¾î°øÇÐ)
- Introduction to Formal Methods
(2009 Fall for graduate students)
¡¡
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
ÃÖ¼ºÀº |
¿ø½ÂÈ£ | ÃÖ¼ºÀº | Á¶½Âö , 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 |