On-The-Fly Verification of Discrete Event Simulations by Means of Simulation Purposes

Paulo Salem da Silva and Ana Cristina Vieria de Melo

Symposium On Theory of Modeling and Simulation - DEVS Integrative M&S Symposium (TMS/DEVS 2011)
Boston, MA, USA, April 4-9, 2011

---

Summary

Discrete event simulations can be used to analyse natural and artificial phenomena. To this end, one provides models whose behaviours are characterized by discrete events in a discrete timeline. By running such a simulation, one can then observe its properties. This suggests the possibility of applying on-the-fly verification procedures during simulations. In this work we propose a method by which this can be accomplished. It consists in modelling the simulation as a a transition system (implicitly), and the property to be verified as another transition system (explicitly). The latter we call a simulation purpose and it is used both to verify the success of the property and to guide the simulation. Algorithmically, this corresponds to building a synchronous product of these two transitions systems on-the-fly and using it to operate a simulator. The precise nature of simulation purposes, as well as the corresponding verification algorithm, are largely determined by methodological considerations important for simulations.

---

START Conference Manager (V2.56.8 - Rev. 1568)