Coloured Petri Net Refinement Specification and Correctness Proof with Coq
In: Proceedings of the First NASA Formal Methods Symposium, 2009-04-01
Online
report
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.
Titel: |
Coloured Petri Net Refinement Specification and Correctness Proof with Coq
|
---|---|
Autor/in / Beteiligte Person: | Choppy, Christine ; Mayero, Micaela ; Petrucci, Laure |
Link: | |
Zeitschrift: | Proceedings of the First NASA Formal Methods Symposium, 2009-04-01 |
Veröffentlichung: | United States: NASA Center for Aerospace Information (CASI), 2009 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|