VIP: A Visual Interface for Promela

Abstract

The Visual Interface to Promela (VIP) tool is a Java based graphical front end to the Promela specication language and the SPIN model checker [2]. VIP supports a visual formalism called v-Promela [3] which extends the Promela lan- guage with a graphical notation to describe structural and behavioral aspects of a system. v-Promela also introduces hierarchical modeling and object-oriented concepts. The formalism is largely consistent with the UML-RT proposal [5] which evolved from the Real-Time Object-Oriented Modeling (ROOM) language [4] and the Unied Modeling Language (UML) [1]. The structural part of a v- Promela model consists of structural elements called capsulesq and describes their interconnection and hierarchical nesting using a variant of UML collaboration diagrams. The behavioral aspects of a v-Promela model are described by hierar- chical communicating extended nite state machines and support such features as group transitions and optional return to history from group transitions.

The VIP tool provides a graphical v-Promela editor supporting point and click editing of v-Promela structure diagrams and hierarchically nested state machines. The editor incorporates syntax checking to warn the user about in- correct use of v-Promela graphical syntax. Storage and retrieval of models is made possible using Java serialization. The tool also has a fully integrated v- Promela compiler which generates Promela code. The resulting Promela models can be analyzed using existing SPIN technology. VIP requires the Java 1.2 Run- time Environment which is available for a variety of operating systems. VIP is not currently publicly available, but expected to be released in the near future.