Title :
An algorithmic procedure for checking safety properties of protocols
Author :
Sabnani, Krishan K. ; Lapone, Aleta M. ; Uyar, M. Ümit
Author_Institution :
AT&T Bell Lab., NJ, USA
fDate :
9/1/1989 12:00:00 AM
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
Keywords :
finite automata; heuristic programming; protocols; ISDN Q.931; algorithmic procedure; alternating bit; finite-state machines; heuristic rules; incremental composition and reduction; protocols; safety properties; Automata; Computer errors; Computer languages; Computer networks; Formal specifications; ISDN; Logic programming; Protocols; Reachability analysis; Safety;
Journal_Title :
Communications, IEEE Transactions on
