Evaluation of protocols from formal specifications: a case study with LAPD

A formal method for the specification and evaluation of protocols is presented, focusing on measures of processing requirements in a node. With this method, it is shown to be possible to define objective measures of protocol performance and to compare implementations of different protocols that provide the same service. As an example, the method is used to specify both the link access protocol on the D-channel (LAPD) and the IEEE 802.2 protocols using the augmented protocol specification language (APSL). The specification consists of a receiver and a transmitter operating concurrently at a given node and of auxiliary processes such as timers. It is also shown that APSL specifications can be used as the starting point for different development paths: automatic generation of software implementation, machine code for hardware implementations, and derivation of performance measures (average and worst-case). The use of APSL allows the use of existing PSL tools for formal verification and the generation of conformance tests. A description of APSL and an overview of LAPD are given