2014
EMSS 2014 Proceeding
Combining DEVS and model-checking: using systems morphisms for integrating simulation and analysis in model engineering
Authors: Bernard P. Zeigler, James J. Nutaro
Abstract
Our objectives here are to discuss the development of a formal framework that exploits the advantages of the Discrete Event System Specification (DEVS) formalism and builds upon recent extensive work on verification combining DEVS and model checking for hybrid systems. The mathematical concepts within the DEVS formalism encompass a broad class of systems that includes multi-agent discrete event components combined with continuous components such as timed automata, hybrid automata, and systems described by constrained differential equations. Moreover, DEVS offers the ability, via mathematical transformations called system morphisms, to map a system expressed in a formalism suitable for analysis (e.g., timed automata or hybrid automata) into the DEVS formalism for the purpose of simulation. Conversely, it is also possible to go from DEVS to formalism suitable for analysis for the purposes of model checking, symbolic extraction of test cases, reachability, among other analysis tasks. We give an example of application of these concepts and discuss the open opportunities for research in model engineering in this direction.
I3M Scientific Sponsors
I3M Industrial Sponsors
I3M Media Sponsors
