Model-checking is a formal verification technique that has been used successfully in verifying software and hardware systems. When a model does not satisfy a property, model checker provides a counterexample. It is an execution path of model which leads the system to the state violating a property. By analyzing the counterexample, we can locate and find potential causes of errors.
In many cases, the length of a counterexample produced by SPIN is too long to analyze. SPIN is a widely used model checker that supports design and verification of asynchronous process system. It has been proven to be effective to find errors of asynchronous systems, such as network protocol. When a system pertains an error, SPIN produces a counterexample. SPIN has an option finding the shortest counterexample in a model. However, the huge cost of iterative search is a problem for users.
This paper presents techniques to reduce the length of counterexample and to visualize a counterexample. With the information of a given counterexample, it detects several identical states and generates a compact counterexample. This technique does not require searching the whole state space. Therefore, it can shorten counterexample with little time and resources. We have visualized a counterexample for efficient counterexample analysis. We have implemented the proposed technique and provided experimental results to prove effectiveness of our approach.
모델 체킹은 하드웨어와 소프트웨어 시스템의 검증에 사용되어 왔다. 만약 시스템에 오류가 있는 경우에 모델 체커는 반례를 생성한다. 이는 모델이 어떤 경로를 통해서 오류 상태에 도달하였는지를 보여 주는 중요한 정보이다. 반례를 분석함으로써 사용자는 오류의 원인을 찾을 수 있다.
많은 경우 스핀에 의해 생성된 반례의 길이가 긴 경우가 많다. 스핀은 산업계에서 많이 사용되는 도구로써 시스템의 검증에 이용된다. 만약 시스템이 속성을 만족하지 않는 경우, 스핀은 반례를 생성한다. 반례는 오류가 발생한 원인을 포함하고 있으나 정확한 이유와 위치는 사용자가 분석 작업을 통해 찾아야 한다. 스핀의 반례는 긴 경우가 많으며 반례의 길이를 줄이기 위한 기능은 사용하기 쉽지가 않다. 모델에서 가장 짧은 반례를 찾기 위해서는 모든 상태 공간을 탐색해야 한다. 또한 방문했던 상태를 여러번 방문해야 하기 때문에 많은 비용이 소요된다.
본 논문에서는 스핀의 반례의 길이를 줄이고 시각화하여 사용자에게 도움을 줄 수 있는 기법을 제공한다. 제공된 반례의 정보를 이용하여 길이를 줄일 뿐만 아니라 시각화를 통하여 분석 작업을 쉽게 할 수 있는 기능을 제안한다. 제안된 기법의 유용성을 확인하기 위해서 구현과 실험을 하였다.
