PROTEAN: a high-level Petri net tool for the specification and verification of communication protocols

Author

Billington, J. ; Wheeler, Geoffrey R. ; Wilbur-Ham, Michael C.

Author_Institution

Comput. Lab., Cambridge Univ., UK

Volume

14

Issue

3

fYear

1988

fDate

3/1/1988 12:00:00 AM

Firstpage

301

Lastpage

316

Abstract

The PROTEAN protocol emulation and analysis computer aid is presented. It is based on a formal specification technique called numerical Petri nets (NPNs), and provides both graphical (color) and textual interfaces to the protocol designer. NPN specifications may be created, stored, appended to other NPNs, structured, edited, listed, displayed, and analyzed. Interactive simulation, exhaustive reachability analysis, and several directed graph analysis facilities are described. Specification languages are compared, with concentration on extended finite state machines and high-level Petri nets. Both the NPN and PROTEAN facilities are described and illustrated with a simple example. The application of PROTEAN to complex examples is mentioned briefly. Work towards a comprehensive protocol engineering workstation is also discussed

Keywords

directed graphs; finite automata; protocols; software tools; PROTEAN; communication protocols; directed graph analysis; engineering workstation; exhaustive reachability analysis; finite state machines; graphical interfaces; high-level Petri net tool; interactive simulation; numerical Petri nets; specification; specification languages; textual interfaces; verification; Analytical models; Automata; Computational modeling; Emulation; Formal specifications; Petri nets; Protocols; Reachability analysis; Specification languages; Workstations;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.4651

Filename

4651