Title :
PROTEAN: A tool for automated protocol analysis
Author :
Lundy, G.M. ; Rothlisberger, M.J.
Author_Institution :
Dept. of Comput. Sci. US Naval Postgraduate Sch., Monterey, CA, USA
Abstract :
A program which performs an automated analysis of a protocol specification is discussed. The input is a protocol specified formally using the systems of communicating machines (SCMs) model and the output is a system and/or global reachability graph, together with any protocol errors which were discovered. The program, called PROTEAN analyzes the protocol for errors such as deadlock and nonexecutable transitions. The SCM model uses a combination of finite state machines and variables, which may be local to a single machine or shared by two or more machines. The current implementation of the model is limited to two-machine protocols. An analysis of a simple data link protocol is included to illustrate the use of the SCM automated model
Keywords :
finite state machines; formal specification; protocols; software tools; PROTEAN; automated protocol analysis; data link protocol; deadlock; finite state machines; global reachability graph; nonexecutable transitions; protocol specification; systems of communicating machines; tool; Automata; Communication networks; Computer networks; Computer science; Performance analysis; Petri nets; Protocols; System recovery; Telecommunication network reliability; Testing;
Conference_Titel :
Computers and Communications, 1993., Twelfth Annual International Phoenix Conference on
Conference_Location :
Tempe, AZ
Print_ISBN :
0-7803-0922-7
DOI :
10.1109/PCCC.1993.344443
