Title :
From DEVS to RTA-DEVS
Author :
Saadawi, Hesham ; Wainer, Gabriel
Author_Institution :
Carleton Univ., Ottawa, ON, Canada
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;
Conference_Titel :
Distributed Simulation and Real Time Applications (DS-RT), 2010 IEEE/ACM 14th International Symposium on
Conference_Location :
Fairfax, VA
Print_ISBN :
978-1-4244-8651-9
DOI :
10.1109/DS-RT.2010.31
