View article

Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even very simple protocols. Consequently, formal specification methods, such as finite-state models, are increasingly being used. The selection/resolution (S/R) model is a finite-state model with a powerful communication mechanism that makes it easy to describe complex protocols as a collection of simple finite-state machines. A software environment, called SPANNER, has been developed to specify and analyze protocols specified with the S/R model. SPANNER provides the facility to compute the joint behavior of a number of finite-state machines and to check if the “product” machine has inaccessible states, states corresponding to deadlocks, and loops corresponding to livelocks. So far, however, SPANNER has had no facility to systematically deal with liveness conditions. For …