Complementarity between simulation and formal verification transformation of PROMELA models into FDDEVS models: Application to a case study

Discrete Event system Specification (DEVS) is a simple comprehensive way to describe complex discrete-event systems in a hierarchical way. Few years ago, Finite and Deterministic DEVS (FDDEVS) was introduced to support verification analysis of a subclass of DEVS problems, in the same way as formal methods. This paper presents guidelines to transform behavioral models used in formal methods like critical sections, especially described in PROMELA in this case, into FDDEVS models, and shows the benefits of such a transformation.