Advanced Software Engineering (고급 소프트웨어공학)
- Formal Methods (Timed Automata & UPPAAL)    
(2013 Fall for graduate students)
　

Course Syllabus
　

2013.01.16 :  홈페이지 구축 중 입니다.
                수업시간: 금 15:00~18:00 새천년관 908호
                한국어 수업입니다. 강의+발표 중심으로 진행됩니다.
2013.04.12 :  정형검증 실습 내용 변경합니다.
                UPPAAL --> SMV
2013.04.12 :  중간고사
                2013.04.26 (월) , 범위: 수업내용 전체
 2013.05.13 :  보강
                2013.05.16 (목) , 12:00 ~ 14:00 , 904호 , 가능한 시간에 오세요. 1:1로 보겠습니다.
                + 그 동안의 발표자료들 모두 제출해 주세요.
2013.06.14 :  보강 (최종발표)
                2013.06.25(화) 09:00~11:00 904호 연구실

               
　

Schedule

Week Date Lecture Presentation
1 03.08    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 

  관련 최신논문 발표 (PDF, PPT)
     - 윤상현 (05.03)

  UPPAAL 소개
     - UPPAAL in a nutshell (STTT 1997)
     - Tutorial

  SMV 소개
     - 김의섭, 박철우, 조은별, 양세옥 (05.03)

  1차 발표 (05.10)
    - 박철우 , 조은별 , 양세옥 , 김의섭 , 서영주

  휴강 (05.17) - 공휴일
  보강 (05.16)
  휴강 (05.24) - ICSE 2013 국제학회 참가

  2차 발표 (05.31)
    - 박철우(smv) , 조은별 , 양세옥 , 김의섭(smv) , 서영주(smv)

  3차 발표 (06.07)
    - 박철우(smv) , 조은별 , 양세옥 , 김의섭(smv) , 서영주(smv,2)
 
  4차 발표 (06.14)
    - 박철우(smv) , 조은별 , 양세옥 , 김의섭(smv) , 서영주(smv)

  최종 발표 (06.25 0900 ~ 11:00 , 904호 연구실)
    - 박철우(smv) , 조은별 , 양세옥
  

2 03.15
3 03.22
4 03.29
5 04.05
6 04.12
7 04.19
8 04.26
9 05.03
10 05.10
11 05.17
12 05.24
13 05.31
14 06.07
15 06.16
16 06.21

　

Term Projects

- 내용:

    - 도구/기법을 선정

    - 선정 도구에 대한 상세한 소개

    - 예제를 하나 정하여, Full Case Study 수행
   - Case Study 주제: 공통 - 커피자판기 (5단계) 

    - 이를 활용한 연구 논문 프로포절 및 논문 제출

　

- 검증도구: SMV

　

- 공통 주제
- 모델: 새천년관 1층 로비에 있는 커피자판기
- 검증속성: 10개 이상

     - 기본기능 --> 잔량/잔액 체크 --> 개별 타이머들 --> 광고기능 --> 모듈화 --> 글로벌 타이머