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.

• Type: Journal
• Year: 2010
• Where: ISSE
• Authors: Christine Choppy, Micaela Mayero, Laure Petrucci
• Keywords: Coq Proof Assistant, ISSE 2010, Refinement Correctness Lemma, Security Privacy, Type Refinement