DocumentCode
1234151
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
Volume
37
Issue
9
fYear
1989
fDate
9/1/1989 12:00:00 AM
Firstpage
940
Lastpage
948
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;
fLanguage
English
Journal_Title
Communications, IEEE Transactions on
Publisher
ieee
ISSN
0090-6778
Type
jour
DOI
10.1109/26.35374
Filename
35374
Link To Document