Sciweavers

ENTCS
2008

Experimenting Formal Proofs of Petri Nets Refinements

13 years 3 months ago
Experimenting Formal Proofs of Petri Nets Refinements
Petri nets are a formalism for modelling and validating critical systems. Generally, the approach to specification starts from an abstract view of the system under study. Once validated, a refinement step takes place, enhancing some parts of the initial model so as to obtain a more concrete specification. Some refinement techniques have been proposed in the framework of high-level Petri to now, proving that a concrete net refines an abstract one, i.e. that there is a refinement relation between them, is completely manual. Our work aims at proving the refinement relation between two nets, both formally and automatically. For that purpose, we use the Coq theorem prover. We aim at having a framework general and parameterised enough to use Coq for any input nets. Moreover, this work constitutes a stepping stone towards bridging the gap between Petri nets and proof assistants techniques, and we claim that theorem proving methods are appropriate to prove the correctness of Petri net refinem...
Christine Choppy, Micaela Mayero, Laure Petrucci
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Christine Choppy, Micaela Mayero, Laure Petrucci
Comments (0)