Title: Combining DEVS and model-checking: concepts and tools for integrating simulation and analysis

Authors: Bernard P. Zeigler; James J. Nutaro; Chungman Seo

Addresses: RTSync Corporation, Arizona Center for Integrative Modelling and Simulation, AZ, USA ' OakRidge National Laboratory, One Bethel Valley Road, Oak Ridge, TN 37831, USA ' RTSync Corporation, Arizona Center for Integrative Modelling and Simulation, AZ, USA

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. 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.

Keywords: model checking; model verification; model validation; cyber-physical systems; CPS; autonomous systems; cooperative systems; systems of systems; modelling; simulation; dynamic systems theory; discrete event system specification; Markov models: lumpable Markov chains; system morphisms.

DOI: 10.1504/IJSPM.2017.082781

International Journal of Simulation and Process Modelling, 2017 Vol.12 No.1, pp.2 - 15

Received: 24 Jan 2015
Accepted: 19 Oct 2015
Published online: 12 Mar 2017 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article