|Start Page Number:||2|
|End Page Number:||15|
|Publication Date:||Mar 2017|
|Journal:||International Journal of Simulation and Process Modelling|
|Authors:||Seo Chungman, Zeigler Bernard P, Nutaro James J|
|Keywords:||engineering, simulation: analysis, markov processes, queues: theory|
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. 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. We discuss a probabilistic extension of the FD‐DEVS formalism that enables a set of model classes and tools derived from Markov‐type models. The MS4 modelling environment provides a suite of tools that support this extension, called FP‐DEVS. In this paper, we describe these tools and the concepts underlying them. We also provide examples of application of these concepts and discuss the open opportunities for research in this direction.