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 nets. Up 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 refinement.