Protocol design: redefining the state of the art
IEEE SoftwarePublished 1 January 1992
Gerard J. Holzmann
Citations28
SJR quartileQ2
SJR score0.56
SNIP1.10
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
The application of formal methods to high-level protocol design is addressed and the framework for proving logical correctness in protocol engineering is discussed.
Abstract
The application of formal methods to high-level protocol design is addressed. A formal method is considered to be one that has the capability of rendering correctness proofs. The traditional and formal design processes are described and compared. The framework for proving logical correctness in protocol engineering is then discussed.>
Keywords
Computer Science
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.
Prentice Hall International (UK) Ltd. eBooksSystematic software development using VDM
1,725 Citations1986Cli B. Jones
Logic of propositions reasoning about predicates functions and operations set notation composite objects and invariants map notation sequence notation data rectification more on data types operation decomposition.
Design and validation of computer protocols
1,695 Citations1991Gerard J. Holzmann
Part 1 Basic: introduction protocol structure error control flow control and design tools: a protocol simulator a protocol validator using the validator.
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.
Journal of the ACMOn Communicating Finite-State Machines
1,067 Citations1983Daniël Brand, P. Zafiropulo
A model of commumcations protocols based on finite-state machines is investigated and it is determined to what extent the problem is solvable, and one approach to solving it is described.
Addison-Wesley Longman Publishing Co., Inc. eBooksTelecommunication networks: protocols, modeling and analysis
902 Citations1986Mischa Schwartz
1. Introduction to Queuing Theory, Layered Architectures in Data Networks, and The Evolution toward Integrated Networks.
Communications of the ACMSolution of a problem in concurrent programming control
762 Citations1983E. Dijkstra
A number of mainly independent sequential-cyclic processes with restricted means of communication with each other can be made in such a way that at any moment one and only one of them is engaged in the “critical section” of its cycle.
Formal Methods in System DesignA stubborn attack on state explosion
572 Citations1992Antti Valmari
The LTL-preserving stubborn set method is presented for reducing the amount of work needed in the automatic verification of concurrent systems with respect to linear-time temporal logic specifications.
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.
Automatic verification of finite state concurrent system using temporal logic specifications
412 Citations1983E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.
Information Processing LettersLimits for automatic verification of finite-state concurrent systems
375 Citations1986Krzysztof R. Apt, Dexter Kozen
Systems which automatically check whether a given finite-state concurrent program satisfies a given temporal formula and allow us to verify the correctness of various nontrivial concurrent programs automatically are developed.
Computer Networks and ISDN SystemsAn introduction to Estelle: A specification language for distributed systems
291 Citations1987Stanislaw Budkowski, Piotr Dembiński
S syntactic and semantic aspects of this description technique are outlined, used to describe the services and protocols of the layers of Open Systems Interconnection (OSI) architecture defined by ISO.
Lecture notes in computer scienceUsing partial orders to improve automatic verification methods
285 Citations2005Patrice Godefroid
Expressing interesting properties of programs in propositional temporal logic
255 Citations1986Pierre Wolper
It is shown that the class of properties of programs expressible in propositional temporal logic can be substantially extended if the authors assume the programs to be data-independent.
Computer NetworksThe CCITT-Specification and Description Language SDL.
148 Citations1989Ferenc Belina, Dieter Hogrefe
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.
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 CommunicationsProtocol Validation by Maximal Progress State Exploration
85 Citations1984Mohamed G. Gouda, Yimin Yu
An efficient variation of state exploration for two communicating finite state machines is discussed, which proposes to divide the task of generating all reachable states into two independent subtasks and only the states reachable by forcing maximal progress for one machine are generated.
Medical Entomology and ZoologyTelecommunications Systems Engineering Using Sdl
84 Citations1989Jared R. W. Smith, Rick Reed
Specification of Telecommunication Systems, a Fully Declarative Specification of a Telecommunication System, and Examples of Structure Representation and System Specification: Defining Sorts from First Principles.
On Limits and Possibilities of Automated Protocol Analysis
83 Citations1987Gerard J. Holzmann
A simple symbolic execution method based on vector addition is extended into a full protocol validator, carefully avoiding known performance bottlenecks and allows validation of protocol systems up to 10 6 states in only minutes of CPU time on a medium size computer.
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.
IRE Transactions on Communications SystemsSDL--CCITT Specification and Description Language
66 Citations1982A. Rockstrom, Roberto Saracco
The background and history of SDL is presented, and its relation to the other languages recommended by CCITT is discussed, and the expected future developments are discussed.
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.
AT&T Technical JournalAlgorithms for Automated Protocol Verification
56 Citations1990Gerard J. Holzmann
The algorithm derived in this manner works in a fixed-size memory arena (it will never run out of memory), it is up to 2 orders of magnitude faster than the previous methods, and it has superior coverage of the state space when analyzing large protocol systems.
AT&T Technical JournalTracing Protocols
55 Citations1985Gerard J. Holzmann
The paper addresses the problem of finding errors in data communication protocols of which the size precludes analysis by traditional means and describes the protocol tracing method, which allows one to locate design errors in protocols relatively quickly by probing a partial state space.
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.
Validating SDL Specifications: an Experiment
47 Citations1989Gerard J. Holzmann, Joanna Patti
A method for validating specifications written in the CCITT language SDL has been implemented as part of an experimental validation system and has been able to perform exhaustive analyses of systems with over 250 million reachable composite system states.
Tools and Rules for the Practicing Verifier
45 Citations1990Zohar Manna, Amir Pnueli
A minimal proof theory which is adequate for proving the main important temporal properties of reactive programs, and illustrates the application of these rules by analyzing and verifying the properties of a new algorithm for mutual exclusion.
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.
Lecture notes in computer scienceUsing partial-order semantics to avoid the state explosion problem in asynchronous systems
38 Citations2005David K. Probst, Hon F. Li
Elsevier eBooksFormal Methods at AT&T - An Industrial Usage Report
26 Citations1992John A. Chaves
The NewCoRe 1 project is developing an approach for the systematic application of formal methods for design and verification specifically for use in the context of large scale software development.
Computer CommunicationsPractical methods for the formal validation of SDL specifications
21 Citations1992Gerard J. Holzmann
Some initial experience is reported on with the application of a formal validation system to SDL design projects involving more than ten people, producing tens of thousands of lines of high-level code over several years.
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.
Acta InformaticaThe complexity of reachability in distributed communicating processes
2 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.