Advanced Software Engineering (고급 소프트웨어공학)
 - Introduction to Model Checking Theories and Tools  
(2017 Spring for graduate students)
 

Course Syllabus
 

+ 논문 쓰기로 한 팀은, 논문 제출 완료 시 A+ 학점 나갑니다.
+ 비논문 제출 팀의 최고 학점은 A
+ 모델링/검증을 수행도 못 해 본 팀은 B 가 최고 학점입니다.

 

Schedule

Week Date Lecture Projects & Presentations
1 03.07    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 

 03.21 - 휴강

 04.18 - 중간고사

 05.30 - 휴강

 06.06 - 휴강 (현충일)
 06.05 - 보강


 06.13 - 기말고사
 06.20 - 최종 발표

2 03.14
3 03.21
4 03.28
5 04.04
6 04.11
7 04.18
8 04.25
9 05.02
10 05.09
11 05.16
12 05.23
13 05.30
14 06.06
15 06.13
16 06.20

 

Team Projects

1차 발표

Introduction
(SMV, SPIN, UPPAAL)
2차 발표

엘리베이터
(SMV, SPIN, UPPAAL)
3차 발표
 
엘리베이터
(보충발표)
4차 발표

프로포절
(1차)
5차 발표

프로포절
(2차 보충)
6차 발표

중간발표
최종발표 논문
04.04 04.25 05.02 05.09  05.16 05.23 06.05 (보강) 06.20
김민우, 이종훈
손준익, 정세진 UPPAAL UPPAAL
이상진, 이종원 SPIN SPIN SPIN 프로포절 V2V 통신의 인증 방식에 대한 검증
노은방, 심우진 SPIN SPIN SPIN 프로포절 프로포절 프로포절 비트코인 GHOST 프로토콜에 대한 검증 논문
박선영, 오예원 SMV SMV SMV 오예원 박선영
박선영
오예원
정형검증도구를 통한 요구공학기술을 연계한 스마트 살충제의 요구사항 분석과 개념적 설계(박선영)
논문(박선영)
이명재, 정혁준 SPIN UPPAAL UPPAAL 프로포절 프로포절 논문
신민용, 안정현 SPIN SPIN SPIN 프로포절 경량 AES 알고리즘(LAS)에 대한 검증
남현우 SMV SMV SMV