HOME > 공학 > 전자공학 > 한국정보처리학회 > 정보처리학회논문지D
기획특집 : 컴포넌트 기술응용 및 프로세스 개선 ; 임베디드 자바 프로그램의 정형 검증
분야 공학 > 전자공학
저자 이태훈 ( Tae Hoon Lee ) , 권기현 ( Gi Hwon Kwon )
발행기관 한국정보처리학회
간행물정보 정보처리학회논문지D 2005년, 제12권 제7호, 931~936쪽(총6쪽)
파일형식 52805097.pdf [다운로드 무료 PDF 뷰어]
판매가격 4,000원
적립금 120원 (구매자료 3% 적립)
이 자료를
논문의 미리보기 2페이지를 PDF파일로 제공합니다.
 
연관 논문
기획특집 : 컴포넌트 기술응용 및 프로세스 개선 ; 일정관리를 위한 Opportunity Tree 및 알고리즘 설계
기획특집 : 컴포넌트 기술응용 및 프로세스 개선 ; 소프트웨어 프로세스 측정을 위한 척도 설계 및 활용
기획특집 : 컴포넌트 기술응용 및 프로세스 개선 ; 금융업무프레임워크에서 컴포넌트 워크플로우 가변성연구
기획특집 : 컴포넌트 기술응용 및 프로세스 개선 ; 국방 CBD 산출물을 위한 정량적 품질 평가 방법
기획특집 : 컴포넌트 기술응용 및 프로세스 개선 ; RAiSE: 다양한 의미론과 사용의 용이성을 제공하는 그래픽 프로세스 모델링 언어
 
 
국문초록
임베디드 소프트웨어는 크기나 기능면에서 복잡하기 때문에 에러가 숨어있을 확률이 높다. 그래서 에러를 효과적으로 찾아낼 수 있는 방법이 절실히 요구된다. 임베디드 소프트웨어에서 잠재적인 오류를 찾아내는 기술중의 하나가 모델 체킹이며, 대표적인 연구로서 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.
 
 
정형 검증, 모델 체킹, 추상화, 자바 프로그램, Formal Verification, Model Checking. Abstraction, Java Program
 
 
도움말
본 논문은 참고용 논문으로 수정 및 텍스트 복사가 되지 않습니다.
 
 
추천자료
[졸업][경영정보] 기업의 M-커머스를 이용한 성공전략
IBM의 국제적 경영 전략과 실현 방안
[졸업][경영정보] M-commerce 모바일커머스 사례분석 및 성공전략에 관한 연구
[정보시스템개론] OODB(Object-Oriented Data Base), 객체지향 데이터 베이스
[경영정보론 MIS] IT서비스 업체 (주)온더아이티 기업 분석 보고서
유비쿼터스정의와 국내외동향
[전자상거래] 정보기술 환경분석
[클라우드 컴퓨팅] 퍼블릭, 프라이빗, 하이브리드 클라우드의 특징과 활용방안
[졸업][경영정보] DSS의 발전 방향과 설계기법에 관한 연구
[경영전략] 전략기법 (ERP, SCM, CRM, EVA, KMS)
오늘 본 자료
오늘 본 자료가 없습니다.
장바구니 담은 자료
장바구니가 비어 있습니다.
이 간행물 인기자료
데이타베이스 : 단축-경로와 확장성 ...
소프트웨어 공학 : 훈련데이터 집합을...
데이터베이스 : 순차패턴에 기반한 XM...
데이터베이스 : 불확실한 시간 간격을...
소프트웨어 공학 : 디자인 패턴에 대...
이 간행물 신규자료
한글 형태소 및 키워드 분석에 기반한...
TK-Indexing: NoSQL 기반 SNS 데이터 ...
UML 상태 기계를 이용한 임베디드 소...
레퍼런스 흐름에 기반한 디자인 패턴...
웹 서비스 합성 구성을 위한 QoS고려 ...
저작권 정보
본 학술논문은 한국학술정보㈜ 각 학회간에 저작권 계약이 체결된 것으로 HAPPY학술이 제공하고 있습니다. 본 저작물을 불법적으로 이용시는 법적인 제재가 가해질 수 있습니다.
 
서비스이용약관 | 개인정보취급방침 | E-mail 수집 거부 | 제휴 및 광고문의 | FAQ
이메일 무단 수집 거부
본 웹사이트에 게시된 이메일 주소가 전자우편 수집 프로그램이나 그 밖의 기술적 장치를 이용하여 무단으로 수집되는 것을 거부하며, 이를 위반시 정보통신망법에 의해 형사처벌됨을 유념하시기 바랍니다. [게시일 2003년 4월 2일]