| 한글제목(Korean Title) |
블록 부호화를 통한 지연 술어 추상화 모델 체킹을 빠르게 하기 위한 에러 위치 지향 순회 전략 |
| 영문제목(English Title) |
Error Location-Directed Traversal Strategy for Fast Lazy Predicate Abstraction Model Checking via Block Encoding |
| 저자(Author) |
이낙원
김문주
백종문
Nakwon Lee
Moonzoo Kim
Jongmoon Baik
|
| 원문수록처(Citation) |
VOL 46 NO. 02 PP. 0269 ~ 0271 (2019. 12) |
한글내용
(Korean Abstract) |
블록 부호화를 통한 지연 술어 추상화 기법 (Lazy Predicate Abstraction via Block Encoding, LPABE)은 추상화 기반 모델 체킹의 추상 상태 폭발 문제를 반복문의 시작지점에서만 추상 상태를 만들고 여러 임시 상태들을 하나로 합침으로써 완화하는 기법이다. 그런데 에러 위치에 빠르게 도달하는 것이 상태의 수를 감소시키는데 효과적임에도 불구하고 LPABE가 기존에 사용하는 순회 전략은 에러 위치에 늦게 도달하는 문제가 있다. 기존 순회 전략은 에러 위치에 도달하는 것과 관련이 없는 반복문들을 반복해서 순회하면서 많은 수의 추상 상태를 만드는 현상을 발생시킬 수 있다. LPABE는 추상 상태를 만드는데 대부분의 시간을 소요하기 때문에 추상 상태의 수를 줄이는 것은 LPABE의 소요시간을 줄이는데 매우 중요하다. 본 연구에서는 LPABE의 소요시간을 줄이기 위해 에러 위치 지향 순회 전략 (Error location-Directed Traversal Strategy, EDTS)을 제안한다. EDTS는 실행 경로들 중에서 에러 위치에 가장 가깝게 도달한 실행 경로를 가장 먼저 탐색함으로써 반복문을 불필요하게 탐색하는 현상을 줄이고자 한다. EDTS를 평가하기 위하여 3831개 벤치마크들을 대상으로 LPABE-EDTS와 LPABE를 비교하는 실험을 수행하였다. 실험 결과 LPABE-EDTS는 LPABE에 비하여 50개 더 많은 벤치마크들을 해결하였으며 같은 벤치마크를 평균적으로 더 적은 시간 만에 해결하였다.
|
영문내용
(English Abstract) |
|
| 키워드(Keyword) |
|
| 파일첨부 |
PDF 다운로드
|
