| 한글제목(Korean Title) |
Statechart 명세의 등가 관계 검사 |
| 영문제목(English Title) |
Equivalence Checking for Statechart Specification |
| 저자(Author) |
박명환
방기석
최진영
이정아
한상용
|
| 원문수록처(Citation) |
VOL 06 NO. 06 PP. 0608 ~ 0619 (2000. 12) |
한글내용
(Korean Abstract) |
본 논문에서는 가상 프로토타입핑의 주요 명세 언어인 Statechart 명세를 프로세스 알제브라의 일종인 ACSR(Algebra of Communicating Shared Resources)로 변환하는 규칙을 제안한다. Statechart는 사용하기 편리하고 이해하기 쉬운 명세 언어이지만 수학적인 semantics의 정의가 되어 있지 않아 명세의 정확성을 검증하기가 매우 어렵다. Statechart 명세를 ACSR로 바꾸게 되면 Statechart에 수학적인 semantics를 주게 되고 VERSA를 이용해서 Statechart 명세를 수학적으로 검증할 수 있게 된다. 따라서, 두 언어의 장점, 즉 Statechart의 편리함과 ACSR의 정확성을 모두 얻을 수 있다.
|
영문내용
(English Abstract) |
In this paper, we give a formal semantics for Statechart via a translation into Algebra of Communicating Shared Resources(ACSR). Statechart is a very rich graphical specification language, which is suitable to specify complicated reactive systems. However, the incorporation of graph into specification and rich syntax makes Statechart semantics very complicated and ambiguous. Thus, it is very difficult to verify the correctness of Statechart specifications. Also, we propose the formal verification method for Statechart specifications by showing equivalence relation between two Statechart specifications. This makes it possible to combine the advantages of a graphical language with the rigor of process algebra.
|
| 키워드(Keyword) |
Statechart 명세
등가 관계
ACSR
|
| 파일첨부 |
PDF 다운로드
|
