추상 도달가능성 그래프 기반 소프트웨어 모델체킹에서의 탐색전략 고려방법 


44권  10호, pp. 1034-1044, 10월  2017
10.5626/JOK.2017.44.10.1034


PDF

  요약

본 연구에서는 추상 도달가능성 그래프(ARG) 기반의 소프트웨어 모델체킹에서 그래프 탐색전략을 설정할 수 있는 새로운 방법을 제시한다. ARG의 여러 실행 경로를 하나로 묶어 모델체킹 성능을 향상시키는 기법인 블록 인코딩(Block Encoding) 기법을 활용하는 경우 기존의 기법들은 인코딩 전의 ARG에서 인코딩을 효과적으로 수행할 수 있는 탐색전략만을 고려하였을 뿐 실제 모델체킹의 성능을 좌우할 수 있는 인코딩 후의 ARG에 대한 탐색전략을 고려하지 못하는 문제가 있었다. 본 연구에서는 기존 연구에서 제시된 탐색 기법을 사용하여 블록 인코딩을 효과적으로 수행하는 동시에 인코딩된 후의 ARG에 대한 탐색 순서를 고려할 수 있는 이중 탐색전략 기법을 제시한다. 또한 탐색 순서의 변화가 모델체킹의 성능에 미치는 영향을 확인하기 위하여 제시하는 기법을 오픈소스 모델체킹 도구에 구현하고 벤치마크 실험을 수행하였으며 탐색전략이 달라지면 모델체킹의 성능이 달라지는 현상을 확인하였다.


  통계
2022년 11월부터 누적 집계
동일한 세션일 때 여러 번 접속해도 한 번만 카운트됩니다. 그래프 위에 마우스를 올리면 자세한 수치를 확인하실 수 있습니다.
  논문 참조

[IEEE Style]

N. Lee and J. Baik, "Controlling a Traversal Strategy of Abstract Reachability Graph-based Software Model Checking," Journal of KIISE, JOK, vol. 44, no. 10, pp. 1034-1044, 2017. DOI: 10.5626/JOK.2017.44.10.1034.


[ACM Style]

Nakwon Lee and Jongmoon Baik. 2017. Controlling a Traversal Strategy of Abstract Reachability Graph-based Software Model Checking. Journal of KIISE, JOK, 44, 10, (2017), 1034-1044. DOI: 10.5626/JOK.2017.44.10.1034.


[KCI Style]

이낙원, 백종문, "추상 도달가능성 그래프 기반 소프트웨어 모델체킹에서의 탐색전략 고려방법," 한국정보과학회 논문지, 제44권, 제10호, 1034~1044쪽, 2017. DOI: 10.5626/JOK.2017.44.10.1034.


[Endnote/Zotero/Mendeley (RIS)]  Download


[BibTeX]  Download



Search




Journal of KIISE

  • ISSN : 2383-630X(Print)
  • ISSN : 2383-6296(Electronic)
  • KCI Accredited Journal

사무국

  • Tel. +82-2-588-9240
  • Fax. +82-2-521-1352
  • E-mail. chwoo@kiise.or.kr