Combining DEVS and model-checking: concepts and tools for integrating simulation and analysis. (2017)

• Record Type: Journal Article
• Authors: Zeigler, Bernard P.; Nutaro, James J.; Seo, Chungman
• Is Part Of: International journal of simulation and process modelling. Volume 12:Number 1(2017)
• Page Start: 2
• Page End: 15
• Publication Date: 2017
• Subjects: 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; Management -- Computer simulation -- Periodicals; Mathematical models -- Periodicals; Operations research -- Periodicals; Simulation methods -- Periodicals; 003.05
• Languages: English
• ISSNs: 1740-2123

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.