Construction and validation of a Petri net model of a layered protocol architecture

A study is made of a three-layer store-and-forward communication protocol as an example of describing systems in layers. The example is comprised of a 'stop and wait' transport layer built on top of an 'Aloha' data link layer implemented on a satellite communication channel; each protocol layer is modeled by a different colored Petri net which is validated independently by verifying basic functionality assertions by inspection of the place and transition invariants. A notion of equivalence in a Petri net is then introduced to study the consistency of the different layers. >