Protocol Modelling and Validation Using Coloured Petri Nets

Author

Bharti, Veena ; Trivedi, M.C. ; Kumar, Sudhakar

fYear

2013

fDate

27-29 Sept. 2013

Firstpage

197

Lastpage

204

Abstract

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.

Keywords

Petri nets; formal verification; protocols; system recovery; RSVP resource reservation protocol; coloured Petri nets; communication protocols; deadlock analysis; formal methods; invariant analysis; liveness analysis; protocol modelling; protocol validation; protocol verification; reachability analysis; Abstracts; Analytical models; Color; Image color analysis; Performance analysis; Protocols; Receivers; Protocol verification; RSVP; coloured Petri nets;

fLanguage

English

Publisher

ieee

Conference_Titel

Computational Intelligence and Communication Networks (CICN), 2013 5th International Conference on

Conference_Location

Mathura

Type

conf

DOI

10.1109/CICN.2013.50

Filename

6657983