Formal Framework for Discrete-Event Simulation

A formal framework for modelling and simulation of parallel systems named ProjectDEVS is presented. The objective of this framework is to apply a Model-Based System Engineering approach to the development of simulation products for cyber-physical embedded systems. It is intended for the design and automated deployment of virtual prototypes. Models are constructed by coupling concurrent components exchanging data through ports and executed by various simulation schemes, namely simulators. This paper focuses on the integration of a Time Petri Net implementation of a parallel simulator into the framework. The semantics of the parallel simulator is formally described using timed transition system to verify the correctness of the implementation. Then, a model with its simulator can be model checked against formal specification and be rapidly deployed on FPGA or PC via code generators. (C) 2017, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd. All rights reserved.