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