생몰정보
소속
직위
직업
활동분야
주기
서지
국회도서관 서비스 이용에 대한 안내를 해드립니다.
검색결과 (전체 1건)
원문 있는 자료 (1) 열기
원문 아이콘이 없는 경우 국회도서관 방문 시 책자로 이용 가능
목차보기더보기
표목차
목차
감사의 글 9
논문개요 10
제1장 서론 12
제1절 연구 배경 12
제2절 연구 목표 14
제3절 논문의 구성 16
제2장 관련 연구 17
제1절 모델 체킹 17
제2절 소프트웨어 모델 체킹 19
제3절 SAT 기반 범위 모델 체킹 28
제3장 SAT 기반 범위 모델 체킹의 적용 32
제1절 BIR의 의미 32
제2절 BIR 모델의 변환 36
제3절 LTL 속성식 변환 43
제4장 멀티 스레드 모델의 검증 45
제1절 하위 표현 구문의 변환 45
제2절 멀티 스레드 모델의 검증 47
제5장 사례 연구 49
제1절 문제 선정 49
제2절 속성 정의 51
제3절 실험 결과 및 고찰 52
제6장 결론 및 향후 연구 53
참고문헌 54
부록 56
Abstract 60
(표 1) 소프트웨어 모델 체킹 도구 13
(표 2) Java Path Finder2의 기본 특성 22
(표 3) SLAM의 기본 특성 23
(표 4) BLAST의 기본 특성 25
(표 5) MAGIC의 기본 특성 26
(표 6) BOGOR의 기본 특성 28
(표 7) 실험 결과 52
(그림 1)/(그림 4) 확장된 BOGOR의 모델 체킹 절차 15
(그림 2)/(그림 5) Java Path Finder2 구성도 21
(그림 3)/(그림 6) 간단한 예제 프로그램 22
(그림 4)/(그림 7) 지연 추상화의 간단한 예 24
(그림 5)/(그림 8) BOGOR의 아키텍쳐 27
(그림 6) SAT 기반 범위 모델 체킹 31
(그림 7) BIR 모델의 표현 방식 33
(그림 8)/(그림 9) BIR 모델의 문법 34
(그림 9)/(그림 10) (a) BIR 모델과 (b) 해당하는 SAT 테이블 37
(그림 10) 2-bit 가산기 42
(그림 11) 하위 표현의 구분 46
(그림 12) 멀티 스레드 모델과 스케쥴링 48
(그림 13) 식사하는 철학자 문제의 변환 과정 49
(그림 14) 2명의 철학자와 2개의 포크를 사용한 식사하는 철학자 문제 50
(그림 15) 1번 철학자의 SAT 테이블 50
원문구축 및 2018년 이후 자료는 524호에서 직접 열람하십시요.
도서위치안내: / 서가번호:
우편복사 목록담기를 완료하였습니다.
* 표시는 필수사항 입니다.
* 주의: 국회도서관 이용자 모두에게 공유서재로 서비스 됩니다.
저장 되었습니다.
로그인을 하시려면 아이디와 비밀번호를 입력해주세요. 모바일 간편 열람증으로 입실한 경우 회원가입을 해야합니다.
공용 PC이므로 한번 더 로그인 해 주시기 바랍니다.
아이디 또는 비밀번호를 확인해주세요
