Abstract

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.

Keywords

Computer scienceFormalism (music)Communications protocolFormal specificationFinite-state machineFormal verificationProgramming languageFormal methodsModel checkingDistributed computingTheoretical computer scienceSoftware engineeringComputer network

Affiliated Institutions

Related Publications

A really temporal logic

Rajeev Alur , T. A. Henzinger

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers ov...

1989 30th Annual Symposium on Foundations ... 162 citations

Publication Info

Year
1982
Type
article
Volume
SE-8
Issue
5
Pages
460-489
Citations
54
Access
Closed

External Links

View on DOI.org

Social Impact

Altmetric
PlumX Metrics

Social media, news, blog, policy document mentions

Citation Metrics

54
OpenAlex

Cite This

Carl A. Sunshine, D.H. Thompson, Roddy W. Erickson et al. (1982). Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models. IEEE Transactions on Software Engineering , SE-8 (5) , 460-489. https://doi.org/10.1109/tse.1982.235736

Identifiers

DOI
10.1109/tse.1982.235736