Protocol Modelling and Validation Using Coloured Petri Nets

The paper deals with the issue of the verification of communication protocols based on integration of formal methods chosen (coloured Petri nets). A method is proposed, that uses the coloured petri net for protocol specification, and transformation rules for a translation of the specification into a Petri net while preserving the semantics of the specification. Coloured Petri nets are well-known formal method for their analytical power to deal with a problem of protocol verification: invariant, reach ability, deadlock and liveness analysis. Elements of theory behind the method are sketched in a short way. The method is illuminated by an example: RSVP Resource Reservation Protocol.