An algorithmic procedure for checking safety properties of protocols
- 1 January 1989
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Communications
- Vol. 37 (9), 940-948
- https://doi.org/10.1109/26.35374
Abstract
A procedure for checking safety properties of communication protocols is presented. A protocol is specified as a collection of communicating finite-state machines (FSMs). Two novel algorithms used in this procedure are described. The first algorithm does incremental composition and reduction of FSMs. It uses three heuristic rules which reduce the number of states in the global FSM by one to two orders of magnitude while maintaining its observational equivalence. The second algorithm checks whether the behavior of one FSM is a subset of another FSM's behavior. This procedure has been applied to the ISDN Q.931 and alternating bit protocols. >This publication has 12 references indexed in Scilit:
- An algorithmic technique for protocol verificationIEEE Transactions on Communications, 1988
- Modular verification of asynchronous networksPublished by Association for Computing Machinery (ACM) ,1987
- Closed Covers: To Verify Progress for Communicating Finite State MachinesIEEE Transactions on Software Engineering, 1984
- Protocol Verification via ProjectionsIEEE Transactions on Software Engineering, 1984
- Automated verification of connection management of NBS class 4 transport protocolPublished by Association for Computing Machinery (ACM) ,1984
- CCS expressions, finite state processes, and three problems of equivalencePublished by Association for Computing Machinery (ACM) ,1983
- Automatic verification of finite state concurrent system using temporal logic specificationsPublished by Association for Computing Machinery (ACM) ,1983
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980
- Communicating sequential processesCommunications of the ACM, 1978
- An Automated Technique of Communications Protocol ValidationIEEE Transactions on Communications, 1978