Technical reports

Extensions to coloured petri nets and their application to protocols

Jonathan Billington

190 pages

This technical report is based on a dissertation submitted May 1990 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Clare Hall.

DOI: 10.48456/tr-222

Abstract

This dissertation develops a net theoretic specification technique for an area known as protocol engineering that covers the life-cycle of protocols. After surveying the application of net theory to protocol engineering, the fundamentals of the specification technique are presented. The technique is based on Jensen’s Coloured Petri Nets (CP-nets).

To increase their expressive power, CP-nets are extended by including place capacities and an inhibitor function, leading to the definition of a class of extended CP-nets, known as P-nets. To allow the analysis techniques developed for CP-nets to be applied to P-nets, a transformation from P-nets to CP-nets is formalised and it is proved that it preserves interleaving behaviour. The transformation is based on the notion of contemporary places (known from Place/Transition-nets) and involves the definition and proof of a new complementary place invariant for CP-nets. A class of P-nets is defined where true concurrency is preserved under the transformation.

A graphical form of P-nets, known as a P-graph, is formally defined, drawing upon the notions developed for algebraic specification of abstract data types. Arc inscriptions are multisets of terms generated from a many-sorted signature. Transition conditions are Boolean expressions derived from the same signature. An interpretation of the P-Graph is given in terms of a corresponding P-net. In the P-Graph, concrete sets are associated with places, and likewise there are concrete initial marking and capacity multisets. P-Graphs are useful for specification at a concrete level, and allow classes of nets, such as CP-Graphs, many-sorted Algebraic nets and many-sorted Predicate/Transition nets, to be defined as special cases. They also provide the basis for a comparison with other high-level nets such as Predicate/Transition nets and Algebraic nets. An extended place capacity notation is developed to allow for the convenient representation of resource bounds in the graphical form.

Abstract P-Graphs are defined in a similar way to P-Graphs, but this time sorts are associated with places, and markings and capacities are defined at the syntactic level. This is useful for more abstract specifications (such as classes of communication protocols) and for their analysis.

Part of the motivation for the extensions to CP-nets has been to develop convenient constructs for the purging of a place’s marking (or part of the marking), by the occurrence of a single transition. This is achieved by equating the inscriptions of the inhibitor and normal arc. Some convenient notation is developed for the P-Graph for purging parts of a place’s marking.

Some simple communications-oriented examples are presented including queues and the Demon Game developed by the International Organisation for Standardisation as a test case for formal description techniques. A major case study of the M-Access service of the Cambridge Fast Ring is specified with the P-Graph to illustrate the utility of a number of the extensions developed for P-nets.

Full text

PDF (16.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-222,
  author =	 {Billington, Jonathan},
  title = 	 {{Extensions to coloured petri nets and their application to
         	   protocols}},
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-222.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-222},
  number = 	 {UCAM-CL-TR-222}
}