기관회원 [로그인]
소속기관에서 받은 아이디, 비밀번호를 입력해 주세요.
개인회원 [로그인]

비회원 구매시 입력하신 핸드폰번호를 입력해 주세요.
본인 인증 후 구매내역을 확인하실 수 있습니다.

회원가입
서지반출
스테이트차트의 실시간 검증을 위한 모델체커의 확장
[STEP1]서지반출 형식 선택
파일형식
@
서지도구
SNS
기타
[STEP2]서지반출 정보 선택
  • 제목
  • URL
돌아가기
확인
취소
  • 스테이트차트의 실시간 검증을 위한 모델체커의 확장
저자명
방호정,홍형석,김태효,차성덕
간행물명
정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용
권/호정보
2004년|31권 6호|pp.773-783 (11 pages)
발행정보
한국정보과학회
파일정보
정기간행물|
PDF텍스트
주제분야
기타
이 논문은 한국과학기술정보연구원과 논문 연계를 통해 무료로 제공되는 원문입니다.
서지반출

기타언어초록

본 연구는 스테이트차트의 실시간 검증을 위한 알고리즘을 제안한다. 스테이트차트는 실시간 반응형 시스템의 명세에 많이 사용되고 있으며 동기적과 비동기적인 두개의 시간모델을 지원한다. 그러나 기존의 스테이트차트에 대한 실시간 검증 방법은 비동기적 시간 모델과 호환되지 않거나, 변수를 모델에 추가함으로써 모텔의 상태 공간을 증가시키는 단점이 있었다. 우리는 기존의 모델 체킹 알고리즘을 확장하여 이러한 문제점을 해결하였다. 확장된 알고리즘은 시간을 증가시키는 전이만을 고려하기 때문에 스테이트차트의 두 가지 시간 모델에 모두 사용할 수 있으며, 시간의 계산이 알고리즘 내부적으로 이루어지기 때문에 모델에 변수를 추가할 필요가 없어 상태공간을 증가시키지 않는다. 본 연구는 이러한 알고리즘을 토대로 기존의 모델 체커인 NuSMV를 확장하였으며, 사례 연구를 통하여 그 유용성을 확인하였다.

기타언어초록

This paper presents a method for real-time verification of Statecharts. Statecharts has been widely used for real-time reactive systems, and supports two time models: synchronous and asynchronous. However, existing real-time verification methods for them are incompatible with the asynchronous time model or increase state space by introducing new variables to the target models. We solved these problems by extending existing model checking algorithms. The extended algorithms can be used with both time models of Statecharts because they consider time increasing transitions only. In addition, they do not increase target state space since they count those transitions internally without additional variables. We extended an existing model checker, NuSMV, based on the proposed algorithms and conducted some experiments to show their advantage.