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

fYear

1993

fDate

23-26 Mar 1993

Firstpage

346

Lastpage

352

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computers and Communications, 1993., Twelfth Annual International Phoenix Conference on

Conference_Location

Tempe, AZ

Print_ISBN

0-7803-0922-7

Type

conf

DOI

10.1109/PCCC.1993.344443

Filename

344443