평탄화를 이용한 계층형 상태 기계의 단계 의미 정의
Definition of Step Semantics for Hierarchical State Machine based on Flattening
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)가 개발되었다. PeaCE 에서는 데이터 흐름과 제어 흐름을 모두 표현할 수 있는데, 제어 흐름은 상태 기계를 확장한 fFSM으로 나타낸다. fFSM은 계층형 상태 기계로서 제어 흐름을 표현하기 위해 많은 구문을 제공하지만, 모델에 대한 의미가 정의되어 있지 않아서 명세를 검증하는데 어려움이 많다. fFSM의 의미를 정의하기 위해서, 본 논문에서는 계층형 상태 기계를 먼저 평탄화한 후에 평탄화된 모델에 대해서 단계 의미를 정의하였다. 그 결과 레이스 조건, 애매한 전이, 순환 전이 등의 주요한 버그들을 정형적으로 검출할 수 있었다.
Abstract
Hardware and software codesign framework called PeaCE(Ptolemy extension as a Codesign Environment) was developed. It allows to express both data flow and control flow which is described as fFSM which extends traditional finite state machine. While the fFSM model provides lots of syntactic constructs for describing control flow, it has a lack of their formality and then difficulties in verifying the specification. In order to define the formal semantics of the fFSM, in this paper, firstly the hierarchical structure in the model is flattened and then the step semantics is defined. As a result, some important bugs such as race condition, ambiguous transition, and circulartransition can be formally detected in the model.
참고문헌 (9)
- D. Kim, "Static Analysis and Automatic Code Synthesis of flexible FSM Model" (2005)
- D. Harel, "a visual formalism for complex systems", 8, pp.231~274 (1987)
- A. Pnueli, "What is in a step:On the semantics of Statecharts", pp.244~264 (1991)
- E. M. Clarke, "Model Checking" (1999), MIT Press
- D. Kim, "System-Level Specification and Co-simulation for Multimedia Embedded Systems" (2004), computer science department
- J. B. Lind-Nielsen, "Verification of Large State", Event Systems, 2000., ~[DOI]
- E. Mikk, "Hierarchical automata as model for statecharts", pp.181~196 (1997)
- J. Lind-Nielsen, "Verification of Large State", Event Systems Using Compositionality and Dependency Analysis, 2001., 5~23[DOI]
- D. Harel, "The STATEMATE semantics of statecharts" (1996)