Sciweavers

Share
ISSE
2010

Coloured Petri net refinement specification and correctness proof with Coq

11 years 2 months ago
Coloured Petri net refinement specification and correctness proof with Coq
In this work, we address the formalisation of symmetric nets, a subclass of coloured Petri nets, refinement in COQ. We first provide a formalisation of the net models, and of their type refinement in COQ. Then the COQ proof assistant is used to prove the refinement correctness lemma. An example adapted from a protocol example illustrates our work.
Christine Choppy, Micaela Mayero, Laure Petrucci
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Where ISSE
Authors Christine Choppy, Micaela Mayero, Laure Petrucci
Comments (0)
books