Protocol Representation with Finite-State Models
IRE Transactions on Communications SystemsPublished 1 April 1980
André Danthine
Citations99
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.
Abstract
A three-layer model of a computer network is used to introduce the concept of interface and of end-to-end protocols. Using a simple interface protocol as example, finite state automaton and Petri nets are introduced. The idea of an interface machine is rejected and the problems related to the transmission medium are approached. End-to end protocols request a global model which includes two local models and a transmission medium model. However, the local model has to be generalized. This eventually leads to the association of the state of the automaton with a context. Petri nets have also to be expanded. Models presented here have been successfully used for modeling transport protocols.
Keywords
Computer Science
ACM Computing SurveysPetri Nets
1,137 Citations1977James L. Peterson
The structure of Petr i nets, thei r markings and execution, several examples of Petm net models of computer hardware and software, and research into the analysis of Pet m nets are presented, as are the use of the reachabil i ty tree and the decidability and complexity of some Petr i net problems.
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)Finite state description of communication protocols
282 Citations1978Gregor von Bochmann
The paper discusses different aspects of protocol validation, some verification tools based on the finite state formalism, and the basic limitations of the finitestate modelling of protocols.
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.
IRE Transactions on Communications SystemsSpecification and Validation of Protocols
90 Citations1979Philip M. Merlin
The "topology" of a protocol is defined, and protocols that are intended to work in a variety of configurations, as well as configurations which may change in time (i.e. "evolving topologies").
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.
Evaluation nets for computer system performance analysis
82 Citations1972Gary J Nutt
Simulation is used for evaluating proposed computer systems and the difficulty of representation and analysis of combination hardware/software systems has increased with the level of sophistication used in their design.
Computer Networks (1976)Verification of protocols using symbolic execution
59 Citations1978Daniël Brand, William H. Joyner
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.
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.
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.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)A graph-model analysis of computer communications protocols.
38 Citations1974J. Postel
Computer Networks (1976)Survey of protocol definition and verification techniques
29 Citations1978Carl A. Sunshine
ACM Computing SurveysData Communication Control Procedures
24 Citations1972Byron W. Stutzman
This paper is a tutorial on the methods used to control the transmission of digital information on data communication links with simple models of data communication systems introduced and terminology for describing their functions and operation established.
IEEE Transactions on Communication TechnologyFunctional Specification of Call Processing by State Transition Diagram
23 Citations1971H. Kawashima, K. Futami +1 more
Rules for writing a diagram and decomposition of states for reduction and simplification of states are some of the topics discussed and the results gained from actual application to local and toll switching systems are shown.
Computer Networks (1976)Modelling and verification of end-to-end transport protocols
22 Citations1978André Danthine, John Bremer
A formal representation model, particularly well adapted to this kind of protocols, but useful also for other protocol types, is introduced and a method for detection of deadlock situations is presented.
Informatik-FachberichteAn Axiomatic Description of the Transport Protocol of Cyclades
18 Citations1976André Danthine, Joseph Bremer
A problem of representation arises at each of the major development phases of a protocol: the definition and testing of the definition, the implementation and tests of the implementation, and the documentation of an implemented protocol.
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 SIGOPS Operating Systems ReviewRepresentation of process synchronization
9 Citations1975Robert C. Chen
Representation of process synchronization
7 Citations1975Robert C. Chen
The author has been working on graph models similar to Petri nets, stressing the ease and convenience of the model as a descriptive device rather than attempting to prove properties such as liveness and safeness.
Finite state automation
7 Citations1970Dines Bjørner
This paper uses essentially the line control procedures which these documents set out to define to arrive at a complete, precise and unambiguous definition of finite state automata.
ACM SIGOPS Operating Systems ReviewCommunication protocols in a network context
6 Citations1975André Danthine, Joseph Bremer
Modeling and Verification of End-to-End Protocols
5 Citations1982André Danthine
Using a simple interface protocol as example, finite state automaton and Petri nets are introduced and compared and the concept of an interface machine is discussed and rejected.
Communication protocols in a network context
5 Citations1975André Danthine, Joseph Bremer
In a distributed computers network based on a packet-swltched communication subnet, it is possible to describe the system as a hierarchical structure and the complete definition of the system will required not only the level 0, 1 and 2 protocols, but also inter-level protocols.