DocumentCode
3106602
Title
From DEVS to RTA-DEVS
Author
Saadawi, Hesham ; Wainer, Gabriel
Author_Institution
Carleton Univ., Ottawa, ON, Canada
fYear
2010
fDate
17-20 Oct. 2010
Firstpage
207
Lastpage
210
Abstract
Rational Time-Advance DEVS (RTA-DEVS) is an extension to DEVS that enables formal verification of simulation models using standard model-checking algorithms and tools. In order to enable formal verification of DEVS models, we introduce a procedure to approximate DEVS with RTA-DEVS. We include conditions for valid approximation and a calculation method for approximation errors that may be introduced. The resulting RTA-DEVS models are behaviorally equivalent to the original DEVS.
Keywords
approximation theory; discrete event simulation; formal specification; formal verification; RTA-DEVS; approximation error; discrete-event modeling specification; formal verification; model checking algorithm; rational time-advance DEVS; simulation model; Analytical models; Approximation error; Automata; Computational modeling; Robustness; Silicon; DEVS; DEVS verification; Discrete event simulation; RTA-DEVS; Timed Automata; UPPAAL; model checking;
fLanguage
English
Publisher
ieee
Conference_Titel
Distributed Simulation and Real Time Applications (DS-RT), 2010 IEEE/ACM 14th International Symposium on
Conference_Location
Fairfax, VA
ISSN
1550-6525
Print_ISBN
978-1-4244-8651-9
Type
conf
DOI
10.1109/DS-RT.2010.31
Filename
5636855
Link To Document