Title: DEv-PROMELA: an extension of PROMELA for the modelling, simulation and verification of discrete-event systems

Authors: Aznam Yacoub; Maamar El Amine Hamri; Claudia Frydman; Chungman Seo; Bernard P. Zeigler

Addresses: Aix-Marseille Université, CNRS, ENSAM, Université de Toulon, LSIS UMR 7296, 13397, Marseille, France ' Aix-Marseille Université, CNRS, ENSAM, Université de Toulon, LSIS UMR 7296, 13397, Marseille, France ' Aix-Marseille Université, CNRS, ENSAM, Université de Toulon, LSIS UMR 7296, 13397, Marseille, France ' RTSync Corp. and Arizona Center for Integrative Modeling and Simulation, University of Arizona, Tucson, AZ, USA ' RTSync Corp. and Arizona Center for Integrative Modeling and Simulation, University of Arizona, Tucson, AZ, USA

Abstract: PROMELA is a well-known formalism for the modelling and the verification of concurrent systems. PROMELA deals with high-level specifications. As a result, PROMELA models are expressed in a high-level abstraction which does not consider explicit representation of time or events for example. But, the efficiency of the processes of verification and validation relies on the accuracy of the models. That is why we propose, in this paper, work to develop a new extension of PROMELA for the modelling of discrete-event systems. The verification of these models is then done by combining formal verification and simulation-based verification using SPIN and the tool DEv-PROMELA Studio, or using any existing DEVS simulators.

Keywords: DEv-PROMELA; simulation; formal verification; verification and validation.

DOI: 10.1504/IJSPM.2017.085564

International Journal of Simulation and Process Modelling, 2017 Vol.12 No.3/4, pp.313 - 327

Received: 28 Apr 2016
Accepted: 22 Jan 2017
Published online: 30 Jul 2017 *

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