|
|
Digital Library of the
European Council for Modelling and Simulation |
|
Title: |
Maximality
Semantic For Recursive Petri Nets |
|
Authors: |
Djamel-Eddine
Saidouni, Messaouda Bouneb, Jean-Michel Ilie |
|
Published in:
|
(2013).ECMS 2013 Proceedings edited
by: W. Rekdalsbakken, R. T. Bye, H. Zhang European Council for Modeling
and Simulation. doi:10.7148/2013 ISBN:
978-0-9564944-6-7 27th
European Conference on Modelling and Simulation, Aalesund, Norway, May 27th –
30th, 2013 |
|
Citation
format: |
Djamel-Eddine
Saidouni, Messaouda Bouneb, Jean-Michel Ilie
(2013). Maximality Semantic For Recursive Petri
Nets, ECMS 2013 Proceedings edited by: W. Rekdalsbakken, R. T. Bye,
H. Zhang, European Council for Modeling and Simulation. doi:10.7148/2013-0544 |
|
DOI: |
http://dx.doi.org/10.7148/2013-0544 |
|
Abstract: |
This paper is in the
framework of the specification and the verification of concurrent dynamic
systems. We are interested by recursive Petri net specification model for which
we define a maximality
semantics. The underlying semantic model is a maximality-based
labeled transition system. For this purpose, we propose a maximality operational semantic for recursive
Petri nets. As an illustration, a system of filling medical bottles is
specified in terms of recursive Petri net and translated to a maximality-based labeled transition system. This later is
used to check the system properties. The properties are expressed using the
CTL logic and verified by means of the FOCOVE tool. |
|
Full
text: |
|
