본문바로가기

자료 카테고리

검색결과

검색결과 (전체 1건)

검색결과제한

열기
논문명/저자명
SAT 기반의 BIR 모델 체킹 도구 / 조민택
발행사항
수원 : 경기대학교 대학원, 2007.2
청구기호
TM 005.1 ㅈ398s
형태사항
vi, 50 p. ; 26 cm
자료실
전자자료
제어번호
KDMT1200725703
주기사항
학위논문(석사) -- 경기대학교 대학원, 소프트웨어공학, 2007.2
원문
미리보기

목차보기더보기

표목차

목차

감사의 글 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

권호기사보기

권호기사 목록 테이블로 기사명, 저자명, 페이지, 원문, 기사목차 순으로 되어있습니다.
기사명 저자명 페이지 원문 기사목차
연속간행물 팝업 열기 연속간행물 팝업 열기