Publication Date:
2018-06-06
Description:
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.
Keywords:
Mathematical and Computer Sciences (General)
Type:
Proceedings of the First NASA Formal Methods Symposium; 156-165; NASA/CP-2009-215407
Format:
application/pdf
Permalink