임베디드 자바 프로그램의 정형 검증 = Formal Verification of Embedded Java Program

국문 초록 (Abstract)

임베디드 소프트웨어는 크기나 기능면에서 복잡하기 때문에 에러가 숨어있을 확률이 높다. 그래서 에러를 효과적으로 찾아낼 수 있는 방법이 절실히 요구된다. 임베디드 소프트웨어에서 잠재적인 오류를 찾아내는 기술중의 하나가 모델 체킹이며, 대표적인 연구로서 SLAM 이 있다. SLAM은 임베디드 C 프로그램의 안전성 속성을 검증하는 소프트웨어 모델 체킹 도구이다. 본 논문에서는 임베디드 자바 프로그램을 검증하는 모델 체킹 도구를 개발했다. SLAM과는 달리 자바 프로그램의 안전성뿐만 아니라 궁극성 속성을 모두 검증할 수 있다. 개발된 모델 체킹 도구를 이용하여 레고 로봇을 제어하는 임베디드 자바 프로그램의 속성을 검증하였다.

다국어 초록 (Multilingual Abstract)

There may be subtle errors in embedded software since its functionality is very complex. Thus formal verification for detecting them is very needed. Model checking is one of formal verification techniques, and SLAM is a well-known software model checking tool for verifying safety properties of embedded C program. In this paper, we develop a software model checker like SLAM for verifying embedded Java program Compared to SLAM, our tool allows to verify liveness properties as well as safety ones. As a result, we verify some desired properties in embedded Java program for controlling REGO robot.

참고문헌 (Reference)

• 1 "Temporal and modal logic" Elsevier 995-1072, 1990.
• 2 "Progress on the State Explosion Problem in Model Checking" 154-169, lncs20002000
• 3 "Programming Lego Mindstorms with Java The Ultimate Tool for Mindstorms Maniacs" Syngress 2002.
• 4 "Modular Verification of Software Components in C" 30 (30): 388-402, 2004.
• 5 "Model checking the garbage collection mechanism of SMV" Elsevier Science Publishers 55 : 2001.
• 6 "Model Checking" MIT Press 1999.
• 7 "Lazy Abstraction" 58-70, 2002.
• 8 "Extracting Finite-state Models from Java Source Code" 2000.
• 9 "Construction of Abstraction State Graphs with PVS" 72-83, 1997.
• 10 "Automatic Predicate Abstraction of C programs" 36 (36): 203-213, 2001.