TOWARDS AN EXTENSION OF PROMELA FOR THE MODELING, SIMULATION AND VERIFICATION OF DISCRETE-EVENT SYSTEMS

Aznam Yacoub (1) , Maamar El Amine Hamri (1) , Claudia Frydman (1) , Chungman Seo (2) , Zeigler Bernard P. (2)

1 LSIS - Laboratoire des Sciences de l'Information et des Systèmes
2 Arizona Center for Integrative Modeling and Simulation

PROMELA is a well-known formalism for the modeling 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 not considers 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 preliminary work to a new extension of PROMELA for the modeling of discrete-event systems. The verification of these models is then done by combining formal verification and simulation-based verification.

Mots clés: DEv-PROMELA; Simulation; Formal Verification; Verification and Validation

Domaines: Modélisation et simulation

Aznam Yacoub, Maamar El Amine Hamri, Claudia Frydman, Chungman Seo, Zeigler Bernard P.. TOWARDS AN EXTENSION OF PROMELA FOR THE MODELING, SIMULATION AND VERIFICATION OF DISCRETE-EVENT SYSTEMS. 27th European Modeling and Simulation Symposium, EMSS 2015, Sep 2015, Bergeggi, Italy. ⟨hal-03555511⟩