Design and validation of computer protocols
Published 1 January 1991
Gerard J. Holzmann
Citations1,695
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
Part 1 Basic: introduction protocol structure error control flow control and design tools: a protocol simulator a protocol validator using the validator.
Abstract
This text is intended as a comprehensive guide to the design and analysis of computer communications protocols. It introduces a sound discipline for the design of complete and consistent protocol systems, independent of where they are used. This volume discusses the fundamental problems of designing logically consistent methods of communication between multiple computer processes. Standard protocol design problems, such as error control and flow control, are covered in detail, but also structured design methods and the construction of formal validation models. The book contains complete listings and explanations of new protocol validation and design tool called SPIN. Author is in charge of protocol design at Bell Labs. Professionals who bought Tanenbaum's COMPUTER NETWORKS, 2/E and Comer's TCP/IP will buy this. This is the first book to cover automated protocol design and validation tools extensively.
Keywords
Computer Science
Bell System Technical JournalA Mathematical Theory of Communication
80,675 Citations1948Claude E. Shannon
North-Holland mathematical libraryThe Theory of Error-Correcting Codes
11,012 Citations1977
This book presents an introduction to BCH Codes and Finite Fields, and methods for Combining Codes, and discusses self-dual Codes and Invariant Theory, as well as nonlinear Codes, Hadamard Matrices, Designs and the Golay Code.
Compilers: Principles, Techniques, and Tools
8,137 Citations1986Alfred V. Aho, Ravi Sethi +1 more
This book discusses the design of a Code Generator, the role of the Lexical Analyzer, and other topics related to code generation and optimization.
The temporal logic of programs
5,586 Citations1977Amir Pnueli
A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.
ACM SIGCOMM Computer Communication ReviewCongestion avoidance and control
5,337 Citations1995Van Jacobson
The measurements and the reports of beta testers suggest that the final product is fairly good at dealing with congested conditions on the Internet, and an algorithm recently developed by Phil Karn of Bell Communications Research is described in a soon-to-be-published RFC.
Series on software engineering and knowledge engineeringData Structures and Algorithms
2,131 Citations2003
The basis of this book is the material contained in the first six chapters of the earlier work, The Design and Analysis of Computer Algorithms, and has added material on algorithms for external storage and memory management.
Communications of the ACMSelf-stabilizing systems in spite of distributed control
2,098 Citations1974Edsger W. Dijkstra
The synchronization task between loosely coupled cyclic sequential processes (as can be distinguished in, for instance, operating systems) can be viewed as keeping the relation “the system is in a legitimate state” invariant.
Kommunikation mit Automaten
2,078 Citations1962C. A. Petri
The theory of automata is shown not capable of representing the actual physical flow of information in the solution of a recursive problem and a theory of communication is proposed that yields a means of representation that with equal rigor and simplicity accomplishes more than the theory of synchronous automata.
The C Programming Language
1,770 Citations1978Brian W. Kernighan, Dennis M. Ritchie
IEEE Transactions on Software EngineeringTesting Software Design Modeled by Finite-State Machines
1,415 Citations1978Tsun S. Chow
The method is based on a result in automata theory and can be applied to software testing and its error-detecting capability is compared with that of other approaches.
Computer Networks and ISDN SystemsIntroduction to the ISO specification language LOTOS
1,293 Citations1987Tommaso Bolognesi, Ed Brinksma
SpringerReferencestructured programming
1,201 Citations2011
Much work is needed to determine how best to design and implement software with reliability, maintainability, and extensibility; there are already some techniques known that contribute materially to these aims.
IEEE Transactions on Software EngineeringProving the Correctness of Multiprocess Programs
1,101 Citations1977Leslie Lamport
The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs, represented by ordinary flowcharts, and no special synchronization mechanisms are assumed.
Bell System Technical JournalA method for synthesizing sequential circuits
997 Citations1955George H. Mealy
A new method of synthesis is developed which emphasizes formal procedures rather than the more familiar intuitive ones, and familiarity is assumed with the use of switching algebra in the synthesis of combinational circuits.
Mathematical ProgrammingMatching, Euler tours and the Chinese postman
987 Citations1973Jack Edmonds, Ellis L. Johnson
The solution of the Chinese postman problem using matching theory is given and the convex hull of integer solutions is described as a linear programming polyhedron, used to show that a good algorithm gives an optimum solution.
IEEE Transactions on CommunicationsA Protocol for Packet Network Intercommunication
803 Citations1974Vinton G. Cerf, Robert E. Kahn
Journal of the Royal Statistical Society Series B (Statistical Methodology)Some Problems in the Theory of Queues
662 Citations1951David G. Kendall
Information and ComputationCCS expressions, finite state processes, and three problems of equivalence
535 Citations1990Paris C. Kanellakis, Scott A. Smolka
Formal Methods in System DesignMemory-efficient algorithms for the verification of temporal properties
498 Citations1992C. Courcoubetis, M. Vardi +2 more
Algorithms are presented that solve the emptiness problem without explicitly constructing the strongly connected components of the graph representing the product automaton by allowing the algorithms to err with some probability.
Communications of the ACMA note on reliable full-duplex transmission over half-duplex links
442 Citations1969Keith A. Bartlett, R.A. Scantlebury +1 more
A simple procedure for achieving reliable full-duplex transmission over half-duple links is proposed and is compared with another of the same type, which has recently been described in the literature.
Computer Networks and ISDN SystemsA protocol test generation procedure
416 Citations1988Krishan Sabnani, Anton Dahbura
A test sequence generated by the procedure given here tours all state transitions and uses a unique signature for each state, called the Unique Input/Output (UIO) sequence, called an input/output behavior that is not exhibited by any other state.
IRE Transactions on Communications SystemsFlow Control: A Comparative Survey
410 Citations1980Mário Gerla, Leonard Kleinrock
This paper describes how flow control can be exercised at various levels in a packet network: hop level, entry-to-exit level, network access level, and transport level, and the interaction between the different levels is discussed.
IEEE Transactions on Software EngineeringFormal methods for protocol testing: a detailed study
388 Citations1989D. Sidhu, T.-K. Leung
This study shows that a test sequence produced by T- method has a poor fault detection capability, whereas test sequences produced by U-, D-, and W-methods have comparable (superior to that for T-method) fault coverage on several classes of randomly generated machines used in this study.
A Formal Approach to Conformance Testing
253 Citations1993Jan Tretmans
IRE Transactions on Communications SystemsFormal Methods in Communication Protocol Design
221 Citations1980Gregor von Bochmann, Carl A. Sunshine
This paper surveys the formal methods being applied to the problems of protocol specification, verification, and implementation, including state transition models, program verification, symbolic execution, and design rules.
NETBLT: a high throughput transport protocol
198 Citations1987David D. Clark, M.L. Lambert +1 more
Communications of the ACMScatter storage techniques
193 Citations1983Robert Morris
L'article donne une presentation didactique sur les methodes connues utilisees par ceux qui ecrivent les assembleurs and compilateurs de maniere a reduire les temps de recherche dans les tables de symboles.
Communications of the ACMAdditional comments on a problem in concurrent programming control
187 Citations1966Donald E. Knuth
Professor Dijkstra's ingenious construction and Hyman's "simplification" for the case of two computers hardly works at all, and it is hoped that this letter can save people some of the problems they would encounter if they were to use either of those methods.
ACM Transactions on Programming Languages and SystemsOn the Construction of Submodule Specifications and Communication Protocols
150 Citations1983Philip M. Merlin, Gregor von Bochmann
A new method for the construction of submodule specifications is described which defines the specification of the additional submodule in the general case where module specifications are given in terms of sets of possible execution sequences, and interaction occurs when several modules participate in the execution of an atomic interaction.
IEEE Transactions on CommunicationsDevelopment of a Spelling List
134 Citations1982Marie McIlroy
How the spelling checker works, how the words were chosen, how it was used to improve itself, and how the (reduced) list of 30000 English words was squeezed into 26000 16-bit machine words are told.
Software Practice and ExperienceAn improved protocol reachability analysis technique
131 Citations1988Gerard J. Holzmann
An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually.
IEEE Transactions on CommunicationsAn Arithmetic Checksum for Serial Transmissions
118 Citations1982John G. Fletcher
An error-detection method for serial transmissions is presented that uses an integer arithmetic checksum that is a bit weaker at detection but is more efficient, thus representing a different and potentially useful choice in rhobust-benefit spectrum.
Transactions of the American Institute of Electrical EngineersCertain Factors Affecting Telegraph Speed
114 Citations1924H. Nyquist
Computer Networks (1976)An improved protocol validation technique
102 Citations1982Jack Rubin, Colin H. West
It is shown that communication between asynchronous processes can be expressed as sequences of nondecomposable, basic interaction which in the general case involve multiple message exchanges.
AT&T Technical JournalSoftware for Analytical Development of Communications Protocols
101 Citations1990Zvi Har'el, Robert P. Kurshan
A way to develop and implement communications protocols so they are logically sound and meet stated requirements and recount the experience of an application of this methodology to develop a new session protocol at an interface of an AT&T product called the Trunk Operations Provisioning Administration System (TOPAS).
Specification and verification of concurrent programs by A ∀ automata
93 Citations1987Z. Monna, Amir Pnueli
It is shown that ∀-automata are as expressive as extended-temporal-logic (ETL), and in some cases provide a more compact representation of properties than temporal logic.
IRE Transactions on Circuit TheoryCanonical Forms for Information-Lossless Finite-State Logical Machines
90 Citations1959David A. Huffman
Journal of the ACMComputer Studies of Turing Machine Problems
87 Citations1965Lin Shen, Tibor Radó
This paper solves a problem relating to Turing machines arising in connection with the Busy Beaver logical game with the help of a computer program, and the values of two very well-defined positive integers are determined to b~ 6 and 21 respectively.
IEEE MicroByte-Wise CRC Calculations
87 Citations1983Aram Perez
A cyclic redundancy code can be calculated on bytes instead of bits to reduce calculation time by a factor of almost four.
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.
IEEE Transactions on Software EngineeringAutomated Protocol Validation in Argos: Assertion Proving and Scatter Searching
77 Citations1987Gerard J. Holzmann
A model in Argos is constructed consisting of a control flow specification and a formal description of the correctness requirements that can be compiled into a minimized lower level description based on a formal model of communicating finite state machines.
Communications of the ACMFurther comments on Dijkstra's concurrent programming control problem
74 Citations1972Murray Eisenberg, Michael R. McGuire
An algorithm whereby N mainly independent computers, with a common data store as their sole means of communication, could contend for exclusive control of any given resource (storage, I/O, etc.) was presented.
Operating System Design
73 Citations2015Douglas E. Comer, Douglas E. Comer
This textbook guides readers through the construction of a traditional process-based operating system using practical, straightforward primitives and imposes a hierarchical design paradigm that organizes the components in an orderly and understandable manner.
IEEE Transactions on ComputersChecking Experiments ror Sequential Machines
69 Citations1971Edward P. Hsieh
Along a parallel line of development, a new procedure, called the state counting method, is presented for detecting faults that can cause an increase in the number of states due to faults.
The importance of the service concept in the design of data communications protocols
65 Citations1985Chris A. Vissers, Luigi Logrippo
The paper argues for an increased role of the service concept, and its underlying architectural concepts, as the proper bases for designing protocol systems as well as suitable specification, verification, and testing techniques.
Computer Networks and ISDN SystemsProtocol validation by fair progress state exploration
57 Citations1985Mohamed G. Gouda, Ji-Yun Han
If the communication of a network of two communicating finite state machines that exchange messages over two one-directional, unbounded, FIFO channels is found to be bounded, then the finite fair reachability graph can be also used to compute the smallest possible capacities for the two channels in the network.
Proceedings of the IEEEA tutorial on protocols
51 Citations1978Louis Pouzin, Horst Zimmermann
The concept of a distributed system architecture provides the framework for layers and protocols to operate across heterotgeneous systems and points to the major impact brought about by protocols in system design.
Algorithms for Automated Protocol Validation
48 Citations1988Gerard J. Holzmann
This paper studies the four basic types of algorithm for the automated validation of the logical consistency of data communication protocols and finds the first for which the search efficiency does not depend of the size of the state space: there is no time penalty for analyzing very large state spaces.
IEEE Transactions on ComputersModeling and Verification of Communication Protocols in Sara: The X.21 Interface
25 Citations1980Razouk, Estrin
This paper models the CCITT X.21 interface specification using a graph model and verifies the behavior of the interface using analysis tools accessible through UCLA's SARA (System Architects' Apprentice) design aid system.
Acta InformaticaThe complexity of reachability in distributed communicating processes
19 Citations1988John H. Reif, Scott A. Smolka
This paper considers the computational complexity of the reachability problem for various models of communicating processes, and demonstrates a very close relationship between the decidable models and Petri nets and Habermann's path expressions.
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 and ISDN SystemsStep-wise validation of communication protocols and services
17 Citations1986Hasan Ural, Robert L. Probert
This approach is based on dynamic comparison and analysis of observable behaviors presented by system functionality representations given at different levels of abstraction, which is extremely flexible, straightforward to use, and particularly appropriate to systems whose externally observable behavior can be modeled by finite state automata.
Computer Networks (1976)A system for testing protocol implementations
16 Citations1982David Rayner
The theoretical basis which has been established for this work is described, which sets the context within which NPL's current system development plan is discussed.
Test design for computer network protocols
15 Citations1984Behçet Sarikaya
This methodology gives complete test coverage of all data flow functions and tests for unspecified cases can be designed using the control and data flow graphs.
Computer Networks (1976)Communication control in computer networks
9 Citations1981Josef Pužman, Radoslav Pořízek
The problem of controlling data exchange in computer networks with respect to real, in particular stochastic, interferences, and user's requirements, expressed by performance criteria, is discussed.
Backward Symbolic Execution of Protocols.
7 Citations1984Gerard J. Holzmann
This paper discusses an alternative search strategy based on backward symbolic execution, which starts with a state that the author knows to be undesirable and executes the protocol backwards, evaluating only undesirable states in an effort to show that they are unreachable.
IEEE Transactions on ComputersFast Burst Error-Correction Scheme with Fire Code
6 Citations1984Wael Adi
A fast burst error-correction decoder is proposed, based on new aspects of the structure of the error syndrome and the parity check matrix of Fire code recently observed by the author, which makes hardware costs relatively low and enables very high-speed decoding.
OhioLink ETD Center (Ohio Library and Information Network)Towards automating protocol synthesis and analysis
5 Citations1989P.-Y.M. Chu
This research provides a protocol algorithm which produces the protocol specification from the given service specification automatically once some additional information about the decision options and initiation option is provided by the protocol designer, and devise an error-recovery transformation procedure.
NASA Technical Reports Server (NASA)The mutual exclusion problem
3 Citations1970Thomas H. Bredt
Procedures to generate control flow tables for the mutual exclusion problem which require the minimum number of internal states are described and it is proved that these procedures given correct control solutions.