Statechart 명세의 등가 관계 검사 = Equivalence Checking for Statechart Specification

국문 초록 (Abstract)

본 논문에서는 가상 프로토타입핑의 주요 명세 언어인 Statechart 명세를 프로세스 알제브라의 일종인 ACSR(Algebra of Communicating Shared Resources)로 변환하는 규칙을 제안한다. Statechart는 사용하기 편리하고 이해하기 쉬운 명세 언어이지만 수학적인 semantics의 정의가 되어 있지 않아 명세의 정확성을 검증하기가 매우 어렵다. Statechart 명세를 ACSR로 바꾸게 되면 Statechart에 수학적인 semantics를 주게 되고 VERSA를 이용해서 Statechart 명세를 수학적으로 검증할 수 있게 된다. 따라서, 두 언어의 장점, 즉 Statechart의 편리함과 ACSR의 정확성을 모두 얻을 수 있다.

다국어 초록 (Multilingual 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.

목차 (Table of Contents)

• 요약
• Abstract
• 1. 서론
• 2. Statechart
• 3. ACSR(Algebra of Communicating Shared Resources)
• 4. 변환 규칙
• 5. 적용 예
• 6. 결론
• 참고문헌
• 부록
• 저자소개