Path abstraction based counterexample checker for abstract model checking

Abstract

모델체킹은 시스템을 검증하기 위한 기법이다. 모델체킹은 시스템이 가질 수 있는 모든 행위를 다 검사하기 때문에 시스템이 위험한 상황에 빠지지 않을 수 있다는 것을 증명 할 수 있다. 그러나 이러한 엄격한 형태의 검사방식 때문에 모델체킹은 높은 연산 능력을 요구한다. 모델체킹을 좀더 실질적으로 사용 할 수 있도록 하기 위하여 CounterExample Guided Abstract Refinement (CEGAR)라는 기법이 제시되었다. 이 기법은 추상화를 통해 모델의 상태공간을 축소하고 이 과정에서 발생 할 수 있는 거짓 반례를 찾아 추상화 정도를 변화시키면서 모델체킹을 수행하는 기법이다. 따라서 거짓 반례를 찾는 것은 CEGAR 기반 모델체킹의 정확성을 위해 반드시 필요한 작업이다. 그러나 이러한 거짓 반례 검출은 반드시 원래의 모델에서 이루어져야 하기 때문에 모델의 크기가 커지고 상태의 수가 많아질수록 많은 연산을 요구하게 된다. 추상화 기법 중 하나인 논리식 기반의 추상화에서 거짓 반례를 검출 하는 기법은 Satisfiability Modulo Theories-solver를 활용한다. 이러한 기법은 논리식 기반의 추상화에 도달 가능성 형태의 속성에 대한 검증에만 적용 가능하다. 좀 더 전통적이고 일반적인 방법은 모델의 상태 공간을 하나씩 검사하면서 거짓 반례를 검출하는 SPLITPATH 기법이 있다. 이 기법은 반례의 길이가 길고 상태의 수가 많아지면 많은 시간을 소요하게 된다. 게다가 해당 기법은 무한반복 형태의 반례를 검사할 경우에 무한반복을 유한 길이의 반례로 풀어내어 연산을 해야 하는 문제가 있으며 풀어낸 반례는 그 길이가 길어질 수 밖에 없다. 이에 반해 병렬 처리를 이용한 거짓 반례 검출 기법은 반례의 길이에 대해 더 효율적인 성능을 보이지만 일부 경우에 반례의 길이에 맞먹는 횟수의 반복 연산을 수행하면서 효율성이 떨어지는 문제가 있다. 따라서 본 연구의 목적은 CEGAR 기반의 모델체킹을 위한 일반적으로 사용 가능하면서 반례의 길이 증가에 대하여 둔감하고 더 적은 횟수의 반복만으로 결과를 얻어낼 수 있는 거짓 반례 검출 기법을 개발하는 것이다. 기법 개발을 위해 거짓 반례를 분석 한 결과 반례의 경로를 부분적으로 따르는 부분적 거짓 경로가 기존 병렬처리 기반 기법의 반복횟수에 영향을 미치는 것을 확인하였다. 이를 해결하기 위해 Path abstraction이라는 상태 이동 경로에 대한 저장 구조를 제안 하였으며 이를 이용하여 부분적 거짓 경로를 더 빠르게 검출 할 수 있도록 하였다. 이 기법은 검사할 반례의 길이의 두 배수 정도의 작업만으로 결과를 얻을 수 있으며 병렬 처리를 이용하여 무한개의 처리기를 가진 경우에 지수적 복잡도의 반복횟수만을 필요로 한다. 이 기법은 CEGAR 기반의 모델체킹을 더욱 다양한 형태의 모델과 속성의 검증에 사용할 수 있도록 도와주며 반례의 길이가 긴 경우와 심지어 무한길이의 반례에도 효과적으로 적용할 수 있는 기법이다. 기법의 검증을 위하여 기존 관련 기법인 SPLITPATH, 병렬 처리 기반 거짓 반례 검출과의 비교 실험을 수행하였다.