DEv-PROMELA: an extension of PROMELA for the modelling, simulation and verification of discrete-event systems Online publication date: Tue, 25-Jul-2017
by Aznam Yacoub; Maamar El Amine Hamri; Claudia Frydman; Chungman Seo; Bernard P. Zeigler
International Journal of Simulation and Process Modelling (IJSPM), Vol. 12, No. 3/4, 2017
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.
Online publication date: Tue, 25-Jul-2017
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Simulation and Process Modelling (IJSPM):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email email@example.com