Verification of protocols using symbolic execution
Computer Networks (1976)Published 1 September 1978
Daniël Brand, William H. Joyner
Citations59
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
This part describes how this method works for communication protocols involving timing assumptions, state changes depending on message contents, unreliable medium, an arbitrary number of communicating processes, etc.
Abstract
A protocol verifier using symbolic execution has been designed and implemented as part of a general verifier (oriented towards microcode). This part describes how this method works for communication protocols involving timing assumptions, state changes depending on message contents, unreliable medium, an arbitrary number of communicating processes, etc. The method can detect design errors such as deadlock and tempo-blocking; in addition the user can add his own assertions to express other desired properties.
Keywords
Computer Science
Communications of the ACMThe structure of the “THE”-multiprogramming system
1,054 Citations1968Edsger W. Dijkstra
A multiprogramming system is described in which all activities are divided over a number of sequential processes, in each of which one or more independent abstractions have been implemented.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)An algebraic definition of simulation between programs
530 Citations1971Robin Milner
A technique is given and illustrated for proving simulation and equivalence of programs; there is an analogy with Floyd''s technique for proving correctness of programs.
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.
Communications of the ACMThe structure of “THE”-multiprogramming system
177 Citations1983Edsger W. Dijkstra
A multiprogramming system is described in which all activities are divided over a number of sequential processes, in each of which one or more independent abstractions have been implemented.
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.
ACM Computing SurveysAn Introduction to Proving the Correctness of Programs
155 Citations1976S. L. Hantler, James C. King
This paper explains, in an introductory fashion, the method of specifying the correct behavior of a program by the use of input/output assertions and describes one method for showing that the program is correct with respect to those assertions.
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.
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).
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.
IEEE Transactions on Software EngineeringA Problem-Reduction Approach to Proving Simulation Between Programs
12 Citations1976Alexander Birman, William H. Joyner
This paper presents a problem-reduction approach to proving simulation, and describes an interactive system designed for this purpose, and presents a concept of equivalence supplied by Milner's definition of simulation between programs.