Formal Methods for Communication Protocol Specification and Verification
Published 1 January 1979
Carl A. Sunshine
Citations10
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
It is vital to specify the services provided by a protocol layer in addition to specifying the cooperating protocol entities which make up the layer, in order to facilitate design of correct protocols.
Abstract
Abstract : Increasingly numerous and complex communication protocols are being employed in distributed systems and computer networks of all types. This Note describes some of the more formal techniques that are being developed to facilitate design of correct protocols. Our major conclusion is that it is vital to specify the services provided by a protocol layer in addition to specifying the cooperating protocol entities which make up the layer. We develop service specifications of several representative protocols by using formal techniques from software engineering such as abstract machines and buffer histories. A survey of protocol verification methods and a bibliography indexed by key phrases are also provided.
Keywords
Computer Science
Communications of the ACMTime, clocks, and the ordering of events in a distributed system
8,437 Citations1978Leslie Lamport
A distributed algorithm is given for synchronizing a system of logical clocks which can be used to totally order the events, and a bound is derived on how far out of synchrony the clocks can become.
Journal of the ACMReaching Agreement in the Presence of Faults
2,364 Citations1980Marshall C. Pease, Robert E. Shostak +1 more
It is shown that the problem is solvable for, and only for, n ≥ 3m + 1, where m is the number of faulty processors and n is the total number and this weaker assumption can be approximated in practice using cryptographic methods.
IRE Transactions on Communications SystemsRecoverability of Communication Protocols--Implications of a Theoretical Study
865 Citations1976Philip M. Merlin, David Farber
The time-Petri net (TPN) appears to be a suitable model for the study of practical recoverable processes and several practical communication protocols are formally designed and analyzed using this new model.
Communications of the ACMFormal verification of parallel programs
791 Citations1976Robert Keller
An induction principle is presented which treats the control and data state sets on the same ground and it is observed that certain correctness conditions can be expressed without enumeration of the set of all possible control states.
Computer Networks (1976)The implementation of reliable distributed multiprocess systems
236 Citations1978Leslie Lamport
Flue gas from the furnace serves to produce high-pressure steam, provide coolant to quench cracked gas, preheat the hydrocarbon-steam feed and aid in driving a turbine-compressor assembly.
Computer Networks (1976)A data transfer protocol
173 Citations1976N.V. Stenning
A protocol for use at the host-host level of computer networks is presented and assertions which reflect important characteristics of the protocol are derived and verified, for a demonstration that cyclic sequence numbers could be used in the protocol without ambiguity.
IRE Transactions on Communications SystemsA Methodology for the Design and Implementation of Communication Protocols
136 Citations1976Philip M. Merlin
This paper presents a coherent method which permits the specification, check out, and implementation of communication protocols, and it is believed that this methodology will facilitate the installation or modification of complex trunk protocols and other communication protocols.
IBM Journal of Research and DevelopmentGeneral Technique for Communications Protocol Validation
133 Citations1978Colin H. West
The validation exhaustively exercises the interaction domain of a system and identifies all occurrences of a number of well-defined error conditions that can detect when individual processes have no predefined response to incoming messages.
Communications of the ACMProof techniques for hierarchically structured programs
111 Citations1977Lawrence Baylor Robinson, Karl Levitt
Preliminary results are encouraging, indicating that the method can be applied to large programs, such as operating systems, and the method is also applicable to semi-automatic and automatic proofs.
IBM Journal of Research and DevelopmentAutomated Validation of a Communications Protocol: the CCITT X.21 Recommendation
87 Citations1978Colin H. West, P. Zafiropulo
The X.21 interface recommended by the International Telegraph and Telephone Consultative Committee (CCITT) has been validated as a test of a recently developed theory and of an implemented system for automated communications protocol validation.
ComputerFormal Techniques for Protocol Specification and Verification
83 Citations1979Sunshine
Certain formal approaches, such as transition techniques and reachability analysis, show promising results when applied to protocol specification and verification.
IRE Transactions on Communications SystemsProtocol Validation by Duologue-Matrix Analysis
58 Citations1978P. Zafiropulo
A technique is described which identifies design errors in protocols based on modeling a protocol as a pair of interacting graphs whereby interaction sequences are represented by path pairs (one path in each graph).
IRE Transactions on Communications SystemsAn Automated Technique of Communications Protocol Validation
57 Citations1978Colin H. West
An implementation of a recent theory of Zafiropulo is described, which defines protocols in terms of the interaction between two directed graphs, and uses set theory and predicate logic to determine all error conditions that can arise.
Interprocess Communication Protocols for Computer Networks
43 Citations1975Carl A. Sunshine
The requirements and performance of protocols for communication between processes in the Host computers attached to the communication system are examined, and the reliability and the efficiency of protocols are discussed.
Computer Networks (1976)Automated protocol validation: One chain of development
41 Citations1978Harry R. Rudin, Colin H. West +1 more
The progress of one research effort in computer-automated protocol validation is summarized, bringing together in one place the results of a number of studies, some published and some to be published but all widely scattered in the literature.
Computer Networks (1976)Survey of protocol definition and verification techniques
29 Citations1978Carl A. Sunshine
BIT Numerical MathematicsVerification of a class of link-level protocols
19 Citations1978Stein Krogdahl
This paper describes a model of a link-level communication line, and defines a set of operations meant to form the basis of data transfer protocols, and shows that all protocols using the given operations as a basis are partially correct.
Computer Networks (1976)Verification and evaluation of communication protocols
15 Citations1978Gérard Le Lann, Hervé Le Goff
Heuristic techniques have been used also to evaluate performances of various flow control mechanisms intended for internode protocols and transport protocols as well as performances as seen by users of computer networks.
A formal approach to the desin and implementation of network communication protocol
11 Citations2005Andy Teng, M.T. Liu
This paper presents a formal model using the context-free grammar (CFG) for the design and implementation of communication protocols, similar to the Backus-Naur Form that has been used to define the syntax of programming languages.
ACM SIGARCH Computer Architecture NewsInterface, a dispersed architecture
8 Citations1976Chris A. Vissers
Design rules for producing logically complete two-process interactions and communications protocols
7 Citations2005P. Zafiropulo
This paper addresses the problem of protocol failures that are caused by logically incompletely specified designs and rules for creating dually complete designs are established and a design methodology based on these rules is proposed.
ACM SIGCOMM Computer Communication ReviewSome linguistical problems about colloquies
1 Citations1975Fabio A. Schreiber