PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols
Issue No. 03 - March (1988 vol. 14)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.4651
<p>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.</p>
graphical interfaces; interactive simulation; specification languages; PROTEAN; high-level Petri net tool; specification; verification; communication protocols; numerical Petri nets; textual interfaces; exhaustive reachability analysis; directed graph analysis; finite state machines; engineering workstation; directed graphs; finite automata; protocols; software tools
G. Wheeler, M. Wilbur-Ham and J. Billington, "PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols," in IEEE Transactions on Software Engineering, vol. 14, no. , pp. 301-316, 1988.