도달가능성 분석에서 유한 및 결정적 DEVS의 전이 시스템 의미

• 영문명: Transition System Semantics of Finite and Deterministic DEVS in Reachability Analysis
• 발행기관: 한국시뮬레이션학회
• 저자명: 이해영(Hae Young Lee)
• 간행물 정보: 『한국시뮬레이션학회 학술대회집』2014년 추계학술대회 발표집, 21~23쪽, 전체 3쪽
• 주제분류: 공학 > 기타공학
• 파일형태: PDF
• 발행일자: 2014.11.08

영문 초록

Reachability analysis of DEVS models has been realized by using model checkers for timed automata (TA) through the conversion of them to TA;or by finding verifiable subclasses of DEVS with the development of analysis methods for them. In this paper;the author studies the semantics of finite and deterministic DEVS (FD-DEVS);which is a verifiable subclass of DEVS;from a viewpoint of a low-level representation of automata;transition systems;so that an atomic FD-DEVS model is interpreted;with respect to reachability analysis;as a transition system. This would mean that;although an analysis method for FD-DEVS was already proposed;reachability of FD-DEVS models can be also analyzed by methods of TA.

목차

1. 서론

2. FD-DEVS 형식론

3. FD-DEVS의 전이 시스템 의미

4. 결론 및 향후 연구

키워드

Discrete event system specification (DEVS) transition systems reachability analysis model checking formal verification