24년 소프트웨어 검증

(Software Verification)

공지  및 숙제

• 숙제 2

  • https://medium.com/@alejandroAttento/markov-chain-from-scratch-26023664e6b5 

  • 위 블로그 등 다양한 문헌 등을 참고하여, DTMC 소개 자료를 작성하여 수업 시간에 발표할 것.

  • 마코프는 Why?(왜) 이 모델을 만들었을까? When?(언제) 이 모델을 사용하면 좋을까? What?(무슨) 예제를 소개할까? How?(어떻게) PRISM 도구로 결과를 보일까? 등을 다루면 좋겠음

  • 2024.10.01(화) 수업 시간에 발표

• SW중심대학 사업단에서 연구실 인턴십 장학금을 (https://swuniv.kyonggi.ac.kr/community/boardDetail?seq=1128) 지원하고 있음.  소프트웨어검증 수업 관련되어 "경기대 SE 연구실" 인턴십으로 논문 작성이나 프로젝트 경험 쌓기 원하는 학생은 이메일로 9월 29일까지 신청할 것.

강의 개요 

• 2024년 2학기 화요일 6,7,8 교시

• 경기대학교 컴퓨터공학 4학년 전공 과목

• 대한민국 SW 품질, 테스트 및 K-안전 산업을 이끌 전문 인력 양성을 위해 2021년도에 신설된 과목 (언론 보도 참고  https://lifenlearning.chosun.com/pan/site/data/html_dir/2023/03/31/2023033101413.html )

강의 목표 

• (Modeling) 검증할 소프트웨어 시스템을 모델링 할 수 있다.

• (Specification) 소프트웨어 시스템의 속성을 명세 할 수 있다.

• (Verification) 추상화된 소프트웨어 시스템 모델이 속성 명세를 만족하는지 검증 할 수 있고. 검증 결과를 설명할 수 있다.

수강 신청시 유의 사항

• 성적 산출 100점 = 중간(30) + 기말(30) + 출석(20) + 과제물및기타(20)

• 과제물및기타 20점 = TOPCIT(10) + 수업내용과제(10)

  • 수강생들은 2024년 10월 12일(예정) 실시되는 TOPCIT 시험을 보아야 합니다 (이미 보았더라도. 이번 가을에 다시 보아야 하며, 이번 가을 획득한 TOPCIT 점수로 과제물및기타 점수 10점을 산출합니다)

• TOPCIT을 왜 보아야 하는지, 어떻게 준비해야 하는지에 대해서 아래 블로그를 참고해 주세요

  • https://swuniv.kyonggi.ac.kr/community/boardDetail?seq=1092

  • https://swuniv.kyonggi.ac.kr/community/boardDetail?seq=1093

1주 검증 기법의 소개 (2024-09-03)

• 수업에서 사용할 오픈 소스 도구 설치

  • https://nusmv.fbk.eu/  에서 최신 NuSMV  도구를 노트북에 설치

  • https://www.prismmodelchecker.org/ 에서 최신 NuSMV  도구를 노트북에 설치 

• 검증의 개요

• 정형 검증과 비정형 검증의 차이점 소개

• testing, simulation, model checking 의 차이점 이해

• 모델 체킹의 작동 방식 소개

2주 모델링 개요 (2024-09-10)

• 트래지션 시스템 소개

• 순차 프로그램의 모델링

• 병행 프로그램의 모델링 기법 이해: 1) 인터리빙, 2) 공유 변수, 3) 핸드쉐이킹

3주 모델 체킹 도구 (2024-09-17)

• 모델 체킹 도구 소개

• PRISM 도구 사용 방법

• PRISM 도구를 사용한 간단한 시스템 검증

• (숙제) TOPCIT 시험을 신청한 후에 신청서 PDF 파일을 LMS로 제출

4주 속성 명세 (2024-09-24)

• 속성이란 무엇인가?

• 항상 참인 불변가설 속성

• 나쁜 상태를 만나지 않는 안전 속성

• 언제가는 좋은 상태를 만나는 궁극 속성

5주 CTL 속성 명세 언어의 구문 및 의미 (2024-10-01)

• CTL 속성 명세 언어의 구문

• CTL 속성 명세 언어의 의미

• PRISM 도구를 활용한 CTL 실습

6주 CTL 모델 체킹 알고리즘 (2024-10-08)

• 모델 체킹 알고리즘 개요

• 레이블링 알고리즘

• 도구를 활용한 CTL 연습

• (TOPCIT 시험)  2024-10-12일 실시 예정

7주 고정점 방식의 CTL 모델 체킹 알고리즘 (2024-10-15)

• 최소 고정점 연산자의 이해

• 최대 고정점 연산자의 이해

• 고정점 계산을 이용한 CTL 모델 체킹 알고리즘

8주 CTL 모델 체킹 알고리즘 문제 풀이 (2024-10-22)

• 최소 고정점 연산자를 이용한 문제 풀이

• 최대 고정점 연산자를 이용한 문제 풀이

• 최소, 최대 고정점 연산자를 혼합한 문제 풀이

9주 Discrete Time Markov Chain 모델링 (2024-10-29)

• 이산 확률 과정 소개

• DTMC 모델링 소개

• Transient Probability 계산법

• Steady-state Probability 계산법

10주 pCTL 모델 체킹 소개 (2024-11-05)

• 이산 시간 확률 모델 체킹 개요

• 넥스트 연산자(X) 모델 체킹 알고리즘

• 언틸 연산자(U) 모델 체킹 알고리즘

11주 pCTL 모델 체킹 실습 (2024-11-12)

• 이산 시간 마코프 모델링 및 검증 I

• 이산 시간 마코프 모델링 및 검증 II

• 이산 시간 마코프 모델링 및 검증 III

12주 Continuous Time Markov Chain 모델링 (2024-11-19)

• 연속 확률 과정 소개

• CTMC 모델링 소개

• 연속 확률 과정에서의 Transient Probability 계산법

• 연속 확률 과정에서의 Steady-state Probability 계산법

13주  pCTL 모델 체킹 소개 (2024-11-26)

• 연속 시간 확률 모델 체킹 개요

• 넥스트 연산자(X) 모델 체킹 알고리즘

• 바운드 및 언바운드 언틸 연산자(U) 모델 체킹 알고리즘

14주  pCTL 모델 체킹 실습 (2024-12-03)

• 연속 시간 마코프 모델링 및 검증 I

• 연속 시간  마코프 모델링 및 검증 II

• 연속 시간  마코프 모델링 및 검증 III

15주간 수업 마무리 (2024-12-10)

• 한 학기 수업 내용 정리

• 수업에서 배운 내용 활용하는 방안 논의

• 기말고사 답안 풀이