| 한글제목(Korean Title) |
프로그램 합성 기법을 이용한 임베디드 소프트웨어의 모델 체킹 효율성 향상을 위한 사례 연구 |
| 영문제목(English Title) |
A Case Study to Improve the Efficiency of Model Checking in Embedded Software Using Program Synthesis |
| 저자(Author) |
김요엘
최윤자
Yoel Kim
Yunja Choi
|
| 원문수록처(Citation) |
VOL 48 NO. 02 PP. 0173 ~ 0175 (2021. 12) |
한글내용
(Korean Abstract) |
C언어로 작성된 임베디드 소프트웨어를 엄밀히 검증하기 위해 모델 검증기 CBMC을 사용할 수 있으나, 소프트웨어가 복잡할수록 검증 효율성이 크게 감소하는 문제가 있었다. 이를 해결하기 위한 방법으로 프로그램 합성 기법을 사용해 검증 대상 함수를 좀 더 단순한 형태의 동일 행위를 갖는 함수로 합성함으로써 검증 시간을 단축하려는 시도가 있었으나, 합성 기법은 큰 사이즈의 배열을 가진 함수의 합성 정확도가 낮아 실제로 검증에 적용하기 어려웠다. 이를 해결하기 위해 본 연구에서는 배열 인덱스 계산식 및 배열 입력 범위 분석을 통해 검증에 필요 없는 입력 범위를 제거하여 합성 난이도를 줄였고, 기존보다 더 정확하면서 간결한 함수를 합성할 수 있었다. 이를 Object Follower 예제에 적용한 결과 CBMC 실행 시간이 10배 이상 단축되었으며, 검증 결과의 신뢰성을 높일 수 있었다. |
영문내용
(English Abstract) |
|
| 키워드(Keyword) |
|
| 파일첨부 |
PDF 다운로드
|
