A Formal Verification Approach for DEVS
Hernan Dacharry and Norbert Giambiasi
Summer Computer Simulation Conference 2007 (SCSC 2007)
San Diego, California (USA), July 15-18, 2007
Abstract
This paper describes several approaches to the formal verification of discrete event systems modeled with the DEVS formalism. We define the operational semantics of the DEVS formalism in terms of a timed transition system, then we characterize a subclass of DEVS models, through the definition of a formalism inspired by DEVS and timed automata, that allows the use of model-checking tools. Finally, we discuss the application of this tools and present a simple example.