An algorithmic technique for protocol verification
- 1 January 1988
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Communications
- Vol. 36 (8), 924-931
- https://doi.org/10.1109/26.3772
Abstract
An algorithmic procedure for protocol verification is presented. A protocol is described as a collection of processes interacting with one another using CSP-type input/output operations. The safety properties of each process are described by a finite-state machine and the liveliness properties of each process by a collection of temporal logic formulas. The required behavior of the protocol is then specified in the same formalism, and the verification procedure can check the description of the protocol for correctness. An experimental implementation of the verification algorithm has been applied to the alternating-bit protocol. >Keywords
This publication has 11 references indexed in Scilit:
- Expressing interesting properties of programs in propositional temporal logicPublished by Association for Computing Machinery (ACM) ,1986
- Closed Covers: To Verify Progress for Communicating Finite State MachinesIEEE Transactions on Software Engineering, 1984
- Protocol Verification via ProjectionsIEEE Transactions on Software Engineering, 1984
- Specifying Concurrent Program ModulesACM Transactions on Programming Languages and Systems, 1983
- Modular Verification of Computer Communication ProtocolsIEEE Transactions on Communications, 1983
- Finite state description of communication protocolsComputer Networks (1976), 1978
- Communicating sequential processesCommunications of the ACM, 1978
- The temporal logic of programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1977
- A note on reliable full-duplex transmission over half-duplex linksCommunications of the ACM, 1969
- Testing and generating infinite sequences by a finite automatonInformation and Control, 1966