HOME > 공학 > 전자공학 > 한국정보처리학회 > 정보처리학회논문지A
기획특집 : 임베디드 시스템 ; 효과적인 임베디드 소프트웨어 설계를 위한 제어흐름 모델의 자동 검증
분야 공학 > 전자공학
저자 박사천 ( Sa Choun Park ) , 권기현 ( Gi Hwon Kwon ) , 하순회 ( Soon Hoi Ha )
발행기관 한국정보처리학회
간행물정보 정보처리학회논문지A 2005년, 제12권 제7호, 563~570쪽(총8쪽)
파일형식 52805042.pdf [다운로드 무료 PDF 뷰어]
판매가격 4,000원
적립금 120원 (구매자료 3% 적립)
이 자료를
논문의 미리보기 2페이지를 PDF파일로 제공합니다.
 
연관 논문
ESTEREL 임베디드 소프트웨어를 위한 모델 기반 테스트 기법 연구 -
간단한 자바프로그램을 위한 CTL 모델 체킹 -
산업용 임베디드 시스템 플랫폼 개발 -
데이터매핑 편집기를 이용한 웹기반 매시업 페이지의 모델 기반 개발 방법 -
철도시스템 소프트웨어 테스트 커버리지 자동화 도구 및 기준 분석 -
 
 
국문초록
하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)에서는 데이터 흐름과 제어 흐름을 모두 표현할 수 있다. PeaCE에서 제어 흐름을 표현하는 fFSM 명세를 정형 검증하기 위해 fFSM의 단계 의미를 정의하였다. 본 논문에서는 이전 연구에서 정의된 정형 의미를 바탕으로 개발한 자동 검증 도구를 소개한다. 이 도구는 내부 모델체커로 SMV를 사용하며 사용자는 직접 논리식을 기술하지 않고도 레이스 조건, 애매한 전이, 순환 전이 등의 주요한 버그들을 검증할 수 있다.
 
 
영문초록
Hardware and software codesign framework called PeaCE(Ptolemy extension as a Codesign Environment) allows to express both data flow and control flow. To formally verify an fFSM specification which expresses control flow in PeaCE, the step semantics of the model was defined. In this paper, we introduce the automatic verification tool developed by formal semantics of previous work. This tool uses the SMV as inner model checker and, through our tool, users can formally verify some important bugs such as race condition, ambiguous transition, and circulartransition without directly writing logical formulae.
 
 
상태 기계, 모델체킹, 자동 검증, 통합 설계, 단계 의미, State Machine, Model Checking, Automatic Verification, Codesign, Step Semantics
 
 
도움말
본 논문은 참고용 논문으로 수정 및 텍스트 복사가 되지 않습니다.
 
 
추천자료
[기업분석]삼성전자 연구
[기업분석]삼성전자 경영분석
[경영정보학] 정보시스템 문제풀이
[철학] 막스베버학자들의 마르크스주의 비판.
[기술경영] 장영실상이 우리나라 기업의 R&D에 미치는 영향력 분석-IR52 장영실상
[사회] 전자 주민 카드
[윤리] 미래의 미디어와 윤리
1998 정보화에 관한 연차보고서
20세기의 얼굴
미래의 사회환경
오늘 본 자료
오늘 본 자료가 없습니다.
장바구니 담은 자료
장바구니가 비어 있습니다.
이 간행물 인기자료
분산 및 병렬처리 : 22n-k×2k 토러스...
분산 및 병렬처리 : 오버레이 링을 이...
컴퓨터시스템 : 인터넷 상의 가변 비...
분산 및 병렬처리 : 후위순회 피보나...
컴퓨터시스템 : FAST: 플래시 메모리 ...
이 간행물 신규자료
그래픽 하드웨어를 이용한 분자용 보...
Haar-Like 특징을 이용한 고성능 보행...
이더넷 네트워크의 시간 동기화 검증...
유해 사이트를 접속하는 안드로이드 ...
인터넷 상품정보 추출을 통한 M-comme...
저작권 정보
본 학술논문은 한국학술정보㈜ 각 학회간에 저작권 계약이 체결된 것으로 HAPPY학술이 제공하고 있습니다. 본 저작물을 불법적으로 이용시는 법적인 제재가 가해질 수 있습니다.
 
서비스이용약관 | 개인정보취급방침 | E-mail 수집 거부 | 제휴 및 광고문의 | FAQ
이메일 무단 수집 거부
본 웹사이트에 게시된 이메일 주소가 전자우편 수집 프로그램이나 그 밖의 기술적 장치를 이용하여 무단으로 수집되는 것을 거부하며, 이를 위반시 정보통신망법에 의해 형사처벌됨을 유념하시기 바랍니다. [게시일 2003년 4월 2일]