Advanced Software Engineering (고급 소프트웨어공학)
- Introduction to Model Checking
Theories and Tools
(2017 Spring for graduate students)
+ 논문 쓰기로 한 팀은, 논문 제출 완료 시 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 - 휴강 (현충일)
|
| 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 |