Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models

摘要

It is becoming increasingly important that communication protocols be formally specified and verified. This report describes a particular approach--the state transition model--using a collection of mechanically supported specification nd verification tools incorporated in a running system called Affirm. Although developed for the specification of abstract data types and the verification of their properties, the formalism embodied in Affirm can also express the concepts underlying state transition machines. Such models easily express most of the events occurring in protocol systems, including those of the users, their agent processes, and the communication channels. The report reviews the basic concepts of state transition models and the Affirm formalism and methodology, and describes their union. A detailed example, the Alternating Bit Protocol, illustrates various properties of interest for specification and verification. Other examples explored using this formalism are briefly described and the accumulated experience is discussed. (Author)