Formal Framework for Discrete-Event Simulation

Vincent Albert (1) , Clément Foucher (1)

1 LAAS-ISI - Équipe Ingénierie Système et Intégration

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.

Mots clés: Time Petri Net; Formal methods; MBSE; Parallel simulator; Discrete-event simulation

Domaines: Modélisation et simulation

Vincent Albert, Clément Foucher. Formal Framework for Discrete-Event Simulation. 20th IFAC World Congress, Jul 2017, Toulouse, France. pp.5812-5817, ⟨10.1016/j.ifacol.2017.08.535⟩. ⟨hal-01562929⟩