Advanced Software Engineering (고급 소프트웨어공학)
- Introduction to Formal Methods
(2011 Fall for graduate students)
2011.08.29 : 09.09 부터는 10:00 에 시작합니다.
2011.09.10 : T5 부터는 09.23 이후에 발표합니다. T1 ~ T4는 09.16에 발표하시면 되겠습니다.
- 발표는 20분 내외로 부탁 드립니다.
- 발표자료는 발표일 오전 09:00 까지 pdf로 보내주시면 홈페이지에 업로드 하겠습니다.
2011.09.15 : 발표 일시는 아래 테이블 확인하세요.
2011.10.26 : 10.28 수업은 아래의 컨퍼런스 참여로 대체합니다. 09:10까지 예문대 1층 소강당으로 와주세요.
UBITA 2011 아시아 컨퍼런스 (프로그램,
포스터)
2011.11.03 : 중간고사는 11.11에 보겠습니다.
중간 Case Study 발표는 11.18 부터 시작합니다. (11.18: T1~T6, 11.25: T7 ~)
출석부
Schedule
| Week | Date | Lecture | Etc. |
| 1 | 09.02 | Course Introduction (Lecture Note) Introduction to Formal Methods (paper, ppt) 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 |
|
| 2 | 09.09 | ||
| 3 | 09.16 | 추석 (09.12~13) / 발표 #1 : 도구소개 | |
| 4 | 09.23 | 발표 #1 : 도구소개 | |
| 5 | 09.30 | ||
| 6 | 10.07 | ||
| 7 | 10.14 | ||
| 8 | 10.21 | ||
| 9 | 10.28 | ||
| 10 | 11.04 | ||
| 11 | 11.11 | 중간고사 (11.11) | |
| 12 | 11.18 | 발표 #2 : Case Study (11.18 ~) | |
| 13 | 11.25 | ||
| 14 | 12.02 | 발표 #3 : 논문 Proposal | |
| 15 | 12.09 | ||
| 16 | 12.16 |
Term Projects
- 내용:
- 도구/기법을 선정
- 선정 도구에 대한 상세한 소개
- 예제를 하나 정하여, Full Case Study 수행
- 이를 활용한 연구 논문 프로포절 및 논문 제출
- 검증도구:
A. SMV
B. SPIN
C. VIS
D. UPPAAL
E. SAT Solver
F. CBMC (HW-CBMC)
G. BLAST
H. SCADE
I. HyTech
J. TIMES
K. SpaceEx
| 팀 | 팀원 | 도구 소개 | Case Study | 연구논문 프로포절 및 최종 발표 |
| T1 | 조재연 | HyTech (09.16) | Car Collision | 최종발표 |
| T2 | 윤상현(청강) | SMT Solver (09.16) | - | |
| T3 | 송승화 | TIMES (09.16) | OFP 프로세스 스케쥴링 분석 | 최종발표 (w 이종훈) |
| T4 | 오향란 | UPPAAL (09.23) | Smartphone controller for UAVs | 최종발표 |
| T5 | 윤상준 , 허주승 | CBMC (09.23) | ARIS 암호화 알고리즘 | 최종발표 |
| T6 | 이동아(청강) , 이종훈 | TIMES (09.23) | - | |
| T7 | 정경헌(휴학) | SPIN (09.30) | - | |
| T8 | 조미영 | SPIN (09.30) | Cooperative Communication | 최종발표 |
| T9 | 김수정 | SMV (09.30) | 화재감지센서 | 최종발표 |
| T10 | 한성근 | CBMC (09.30) | 최종발표 | |
| T11 | 디부다 우다얀 | SCADE (09.30) | 항공기 컨트롤러 모델링 및 검증 | 최종발표,1,2,3 |