모델 체킹에서 안전성 위반에 대한 효율적인 반례 생성
Efficient Counterexample Generation for Safety Violation in Model Checking
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
모델 체킹은 주어진 모델과 속성간의 만족성 관계를 검사한다. 만일 모델이 속성을 만족하지 않는 경우, 모델 체킹은 그 이유를 담은 반례를 생성한다. 반례는 모델의 디버깅에 사용되며 모델을 이해하는데 도움을 주기 때문에, 반례 생성은 모델 체킹의 필수 구성 요소 중의 하나이다. 본 논문에서는 모델 체킹에서 안전성 속성이 위반되었을 때 그에 대한 반례를 효율적으로 생성하는 방법을 제시하였고, 푸쉬 푸쉬 게임 풀이에 제안한 방법을 적용했다. 그 결과, 기존 NuSMV로는 전체 50게임 중에서 42게임밖에 풀지 못했으나 본 논문의 방법으로는 50게임을 모두 풀었다. 뿐만 아니라, 반례 생성에 소요된 시간과 메모리 사용량이 기존 NuSMV에 비해서 각각 86%와 62% 개선되었다.
Abstract
Given a model and a property, model checking determines whether the model satisfies the property. In case the model does not satisfy the property, model checking gives a counterexample which explains where the violation occurs. Since counterexamples are useful for model debugging as well as model understanding, counterexample generation is one of the indispensable components in the model checking tool. This paper presents efficient counterexample generation techniques when a safety property is falsified. These techniques are used to solve Push Push games which consist of 50 games. As a result, all the games are solved with the proposed techniques. However, with the original NuSMV, 42 games are solved but 8 failed. In addition, we obtain 86% time improvement and 62% space improvement compared to the original NuSMV in solving the game.
참고문헌 (20)
- E. M. Clarke,E. A. Emerson,and A. P. Sistla, "Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications", 8(2), pp.244~263 (1986)
- T. Kropf, "Introduction to Formal Hardware Verification" (1999), Springer
- K. Laster, "Modular model checking of software", lncs 1384, pp.20~35 (1998)
- N. Heintze, "Model checking electronic commerce protocols", pp.147-164, pp.1996~
- 권기현, "모델 검증을 이용한 게임 풀이", 21(1), pp.7~14 (2003)
- A. Cimatti, "Conformant Planning via Symbolic Model Checking", 13, pp.305~338 (2000)
- E. M. Clarke, "Model Checking" (1999), MIT Press
- A. Cimatti, "An OpenSource Tool for Symbolic Model Checking", pp.~2 (2002)
- W. Chan, "Symbolic Model Checking for Large Software Specifications" (1999), University of Washington
- M. B. Dwyer, "Property specification patterns for finite-state verification" (1998)
- G. Kwon, "Applying Model Checking Techniques to Push Push Game Solving", lncs 3026, pp.290~303 (2003)
- E. M. Clarke, "Efficient Generation of Counterexamples and Witness in Symbolic Model Checking", pp.427-432, pp.1995~
- E. M. Clarke,O. Grumberg,and D. E. Long, "Model Checking and Abstraction", 16(5), pp.1512~1542 (1994)
- 권기현, "모델 체킹에서 상태 투영을 이용한 모델의 추상화", 11-d(6), pp.1295~1300 (2004)
- 권기현, "게임 풀이를 위한 NuSMV의 효율적인 반례 생성", 10-d(5), pp.813~820 (2003)
- R. E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation", 35(8), pp.677 1986~691
- E. M. Clark, "Tree-Like Counterexamples in Model Checking", pp.19-29, pp.2002~
- M. Chechik, "Proof-Like Counterexamples", lncs 2619, pp.160~175 (2003)
- P. E. Ammann, "Using Model Checking to Generate Tests from Specifications", pp.46~54 (1998)
- E. M. Clarke, "Counterexample-Guided Abstraction Refinement", pp.154~169 (2000)