TY - GEN
T1 - Combining devs and model-checking
T2 - 26th European Modeling and Simulation Symposium, EMSS 2014
AU - Zeigler, Bernard P.
AU - Nutaro, James J.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84912079289&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84912079289
T3 - 26th European Modeling and Simulation Symposium, EMSS 2014
SP - 350
EP - 356
BT - 26th European Modeling and Simulation Symposium, EMSS 2014
A2 - Merkuryev, Yuri
A2 - Zhang, Lin
A2 - Jimenez, Emilio
A2 - Longo, Francesco
A2 - Affenzeller, Michael
A2 - Bruzzone, Agostino G.
PB - Dime University of Genoa
Y2 - 10 September 2014 through 12 September 2014
ER -