Verification of the AX.25 link-layer protocol using place-transition petri nets - Festin, Cedric Angelo Mojica (1996)
This study is an investigation of the use of Place-Transition Petri nets or simply Petri nets, in modeling and in analyzing communication protocols. The AX.25 Amateur Packet-Radio Link-Layer Protocol Version 2.0 was used as the case study of this thesis. Petri net models were built for the link connection establishment phase, the information transfer phase, the frame rejection phase, and the link disconnection phase of the AX.25 link-layer protocol. In this study of communication protocols using Petri nets, three properties are of interest, namely, boundedness, safety, and liveness or the absence of deadlocks. The main technique for analyzing these properties is the reachability analysis. Reachability analysis is based on exhaustively exploring all possible outcomes the protocol may achieve. One problem associated with this method is the "state space explosion." There are two approaches to solve this problem. The first one is to partition the Petri net model to smaller components so that reachability analysis can be performed. The second approach is to reduce the model into a simpler but equivalent model. This method is called the reduction technique. Both of these approaches were used in this investigation. Pesim, a Petri net software too, proved invaluable as an aid to the analysis of the Petri net models. The analysis shows that the models for the link connection establishment phase, the frame rejection phase, and the link disconnection phase are deadlock free, bounded and safe. However, the analysis for the information transfer phase shows it is deadlock free, 3-bounded but unsafe. With these findings, it can be said that the AX.25 link layer protocol is deadlock free, n-bounded, and unsafe.