This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models
September 1982 (vol. 8 no. 5)
pp. 460-489
C.A. Sunshine, Information Sciences Institute, University of Southern California
It is becoming increasingly important that communication protocols be formally specified and verified. This paper describes a particular approach-the state transition model-using a collection of mechanically supported specification and 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 paper 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 varous properties of interest for specification and verification. Other examples explored using this formalism are briefly described and the accumulated experience is discussed.
Index Terms:
verification, Abstract data types, algebraic axiomatic specifications, alternating bit protocol, natural-deduction theorem-proving, protocols, specification, state transition models
Citation:
C.A. Sunshine, D.H. Thompson, R.W. Erickson, S.L. Gerhart, D. Schwabe, "Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models," IEEE Transactions on Software Engineering, vol. 8, no. 5, pp. 460-489, Sept. 1982, doi:10.1109/TSE.1982.235736
Usage of this product signifies your acceptance of the Terms of Use.