Equivalent Semantic Translation from Parallel DEVS Models to Time Automata
| 详细信息 | 推荐本文 | |
- 作者：Shoupeng Han ; Kedi Huang
- 关键词：Discrete Event System Specification (DEVS) ; Timed Transition System (TTS) ; Semantic Equivalence ; Timed Automata (TA)
- 刊名：Lecture Notes in Computer Science
- 出版时间：2007
- 出版年：2007
- 期刊代码：99_0302-9743
- 类别：cp
- 卷：4487
- 期：1
- 页码：1246-1253
- 数据来源：sp
摘要
Dynamic reconfigurable simulation based on Discrete Event System Specification (DEVS) requires efficient verification of simulation models. Traditional verification method of DEVS model is based on I/O test in which a DEVS model is regarded as a black box or a grey box. This method is low efficient and insufficient because input samples are often limited. This paper proposes a formal method which can translate Parallel DEVS model into a restrict kind of Timed Automata (TA) with equivalent behaviors. By this translation, a formal verification problem of Parallel DEVS model can be changed into the formal verification of according timed automata.