SCSC 2007 START Conference Manager    

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


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.

START Conference Manager (V2.54.4)