BIR 모델의 바운디드 모델 검증 = Bounded Model Checking BIR Model

국문 초록 (Abstract)

하드웨어 검증에서 성공적으로 적용되었던 모델 검증 기법을 소프트웨어 검증에 활용하는 연구가 활발하다. 이러한 연구 중의 하나가 바운디드 모델 검증이다. 바운디드 모델 검증에서는 모델이 갖는 상태 공간을 한꺼번에 모두 탐색하기 보다는 모델의 탐색 범위를 점진적으로 넓혀가면서 에러를 찾는다. 본 논문에서는 이러한 바운디드 모델 검증을 이용하여 BOGOR의 입력 언어인 BIR를 검증하였다. 그 결과 BOGOR에서 제공되는 명시적 모델 검증 기능 보다 우수한 성능을 보였다. 본 논문에서는 BIR 언어를 CNF 논리식으로 변환하는 방법과 단계적 절차를 기술한다.

다국어 초록 (Multilingual Abstract)

Model checking has been successfully applied to hardware verification. Software is more subtle than hardware with respect to formal verification due to its infinite state space. Although there are many research activities in this area, bounded model checking is regarded as a promising technique. Bounded model checking uses an upper bound to unroll its model, which is the main advantage of bounded model checking compared to other model checking techniques. In this paper, we applied bounded model checking to verify BIR which is the input model for the model checking tool BOGOR. Some BIR examples are verified with our technique. Experimental results show that bounded model checking is better than explicit model checking provided by BOGOR. This paper presents the formalization of BIR and the encoding algorithm of BIR into CNF.

목차 (Table of Contents)

• 요약
• Abstract
• 1. 서론
• 2. 바운디드 모델 검증
• 3. BIR 모델
• 4. CNF 변환
• 5. 사례연구
• 6. 결론 및 향후 연구
• 참고문헌

참고문헌 (Reference)

1 "Symbolic Model Checking without BDDs" 193 (193): 1999

2 "Progress on the State Explosion Problem in Model Checking" 176-194, 2001

3 "Model Checking C Source Code for Embedded Systems" 2005

4 "Model Checking" MIT Press 1999

5 "Efficient Computation of Recurrence Diameters" 298-309, 2003

6 "Counterexample-Guided Abstraction Refinement" 154-169, 2000

7 "Construction of Abstract State Graphs with PVS" 72-83, 1997

8 "Bounded Model Checking" 58 : 118-149, 2003

9 "Bogor: An Extensible and Highly-Modular Software Model Checking Frame work" 267-276, 2003

10 "Available at the website http" -6,