| |
| 국문초록 |
| 임베디드 소프트웨어는 크기나 기능면에서 복잡하기 때문에 에러가 숨어있을 확률이 높다. 그래서 에러를 효과적으로 찾아낼 수 있는 방법이 절실히 요구된다. 임베디드 소프트웨어에서 잠재적인 오류를 찾아내는 기술중의 하나가 모델 체킹이며, 대표적인 연구로서 SLAM 이 있다. SLAM은 임베디드 C 프로그램의 안전성 속성을 검증하는 소프트웨어 모델 체킹 도구이다. 본 논문에서는 임베디드 자바 프로그램을 검증하는 모델 체킹 도구를 개발했다. SLAM과는 달리 자바 프로그램의 안전성뿐만 아니라 궁극성 속성을 모두 검증할 수 있다. 개발된 모델 체킹 도구를 이용하여 레고 로봇을 제어하는 임베디드 자바 프로그램의 속성을 검증하였다. |
| |
| |
| 영문초록 |
| 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. |
| |
| |
| 도움말 |
| 본 논문은 참고용 논문으로 수정 및 텍스트 복사가 되지 않습니다. |
| |
|
 |
|
|
|
|
|
|
|
|
| 저작권 정보 |
|
| 본 학술논문은 한국학술정보㈜ 각 학회간에 저작권 계약이 체결된 것으로 HAPPY학술이 제공하고 있습니다. 본 저작물을 불법적으로 이용시는 법적인 제재가 가해질 수 있습니다. |
|
|
|
분야
52805097.pdf 
