Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-72584-8_162 | International Conference on Computational Science (1) |
Keywords | Field | DocType |
formal method,parallel devs model,simulation model,formal verification problem,efficient verification,equivalent semantic translation,dynamic reconfigurable simulation,black box,traditional verification method,parallel devs models,time automata,formal verification,devs model,semantic equivalence | Black box (phreaking),Mathematical optimization,Programming language,SP-DEVS,Computer science,Automaton,Parallel computing,Semantic equivalence,DEVS,Semantic translation,Formal methods,Formal verification | Conference |
Volume | ISSN | Citations |
4487 | 0302-9743 | 4 |
PageRank | References | Authors |
0.42 | 4 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shoupeng Han | 1 | 4 | 0.42 |
| Kedi Huang | 2 | 79 | 11.95 |