Software Verification (¼ÒÇÁÆ®¿þ¾î °ËÁõ)
- Introduction to Software Testing & Formal Methods      

(Spring 2009)

¡¡

Course Syllabus

2009.03.11 :  ÆÀ±¸¼º ¿Ï·á µÇ¾ú½À´Ï´Ù.
2009.03.23 :  ½Ç½À°ü·Ã ÆÀº° ¹ÌÆà ½ºÄÉÁì (Àå¼Ò: 904È£):
                 - 03.24(È­) 17:00 ~ 18:00  1Á¶,  18:00 ~ 19:00 2Á¶, 19:00 ~ 20:00 3Á¶
                 - 03.25(¼ö) 17:00 ~ 18:00  4Á¶,  18:00 ~ 19:00 5Á¶, 19:00 ~ 20:00 6Á¶ 
2009.03.30 :  °øÇÐÀÎÁõ »çÀü¼³¹® ºÎŹ µå¸³´Ï´Ù.
2009.04.08 :  04.13(¿ù)¿¡ ¼ö¾÷ÇÕ´Ï´Ù. 04.15(¼ö)¿¡´Â ±³¼ö ¾øÀÌ ÀÚü ½Ç½ÀÇÕ´Ï´Ù.
2009.04.13 :  Áß°£°í»ç´Â 04.20(¿ù) ¼ö¾÷½Ã°£ÀÔ´Ï´Ù. Open books & Slides.
                ½ÃÇè¹üÀ§: 1Àå~8Àå
2009.04.13 :  ½Ç½À#3´Â Ãë¼ÒÇÏ°í ½Ç½À#2¿¡ ÁýÁßÇÏ°Ú½À´Ï´Ù. ^^;
2009.04.13 :  ¿¹Á¤µÇ¾î ÀÖ´ø ÈÞ°­ÀÏÁ¤ Á¶Á¤ÇÏ¿´½À´Ï´Ù.
2009.04.13 :  ¿¹ºñ±ºÈÆ·ÃÀ¸·Î 04.27(¿ù) ÈÞ°­ÇÕ´Ï´Ù.
2009.04.18 :  Áß°£°í»ç °ü·Ã - ½ÃÇè¹®Á¦ 8¹®Ç× ÀÔ´Ï´Ù.
2009.04.21 :  °øÇÐÀÎÁõ Áß°£¼³¹® ºÎŹ µå¸³´Ï´Ù.
2009.04.24 :  Áß°£°í»ç ¼ºÀû È®ÀÎÇϼ¼¿ä.
2009.04.27 :  °­Àdz»¿ë º¯°æµÇ¾ú½À´Ï´Ù. SMV Model Checking °ü·Ã ÀÌ·Ð ¼ö¾÷À» º¸°­ÇÕ´Ï´Ù.
2009.05.23 :  °­ÀÇ/½Ç½À³»¿ë Ãà¼ÒµÇ¾ú½À´Ï´Ù. ½Ç½À#2·Î ÃÖÁ¾ Æò°¡ÇÏ°Ú½À´Ï´Ù.
2009.06.08 :  °øÇÐÀÎÁõ ÃÖÁ¾¼³¹® ¹× °­ÀÇÆò°¡ ºÎŹ µå¸³´Ï´Ù.
2009.06.08 :  2009.06.09 ÇÏ·ç Á¾ÀÏ Áú¹®ÇÏ·¯ ¿À¼¼¿ä.
                ±â¸»°í»ç´Â ÇÑ ¹®Á¦ ÃâÁ¦ÇÕ´Ï´Ù. ¹®Á¦´Â ÀÌ¹Ì ¾Ë·Á µå·È½À´Ï´Ù.
                Ãâ¼®ºÎ¿¡ ÇÁ·ÎÁ§Æ® Á¡¼ö °ø°³µÇ°í ÀÖ½À´Ï´Ù.
2009.06.08 :  ±â¸»°í»ç´Â 2009.06.15(¿ù) ¼ö¾÷½Ã°£ ÀÔ´Ï´Ù.
2009.06.16 :  ±â¸»°í»ç ¹× ÃÖÁ¾ÇÐÁ¡ °øÁöµÇ¾ú½À´Ï´Ù. ÇÑ Çб⠵¿¾È ¼ö°íÇϼ̽À´Ï´Ù.
               
Ãâ¼®ºÎ

¡¡

Schedule

WEEKS

DATE

LABORATORY (Monday)

LECTURE (Wednesday)

1

03.02 / 03.04

Course Introduction

Chapter 1. Software Test and Analysis in a Nutshell (fig)

2

03.09 / 03.11


Practice #1 (NuSCR)
Practice #1 (NuSCR - revised)
Introduction to Formal Specification

3

03.15 / 03.18

Chapter 2. A Framework for Test and Analysis
Chapter 3. Basic Principles

4

03.23 / 03.25 Chapter 4. Test and Analysis Activities Within a Software process

5

03.30 / 04.01 Practice #2 (SMV) Chapter 5. Finite Models

6

04.06 / 04.08 Chapter 6. Dependence and Data Flow Models

7

04.13 / 04.15 Chapter 8. Finite State Verification

8

04.20 / 04.22 Mid-Term Exam.

9

04.27 / 04.29 ÈÞ°­ - ¿¹ºñ±º ÈÆ·Ã SMV ½Ç½À º¸°­

Software Verification ÀÌ·Ð
   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
¡¡

10

05.04 / 05.06 Practice #2 (SMV) continued.

½Ç½ÀÀÚ·á Ãß°¡
SMV ¸Å´º¾ó, Æ©Å丮¾ó

11

05.11 / 05.13

12

05.18 / 05.20

13

05.25 / 05.27

14

06.01 / 06.03

15

06.08 / 06.10 Practice #2 - Final Presentation & Demo
  T1 : ¹ßÇ¥ÀÚ·á 2, NuSCR ÆÄÀÏ
  T2 : ¹ßÇ¥ÀÚ·á, NuSCR ÆÄÀÏ
  T3 : ¹ßÇ¥ÀÚ·á, NuSCR ÆÄÀÏ
  T4 : ¹ßÇ¥ÀÚ·á, NuSCR ÆÄÀÏ
  T5 : ¹ßÇ¥ÀÚ·á, NuSCR ÆÄÀÏ
  T6 : ¹ßÇ¥ÀÚ·á, NuSCR ÆÄÀÏ

16

06.15 / 06.17 Final Exam.

¡¡

 

¡¡