VIP - A Visual Interface for Promela

We are developing the VIP toolset. VIP supports the v-Promela language, a visual, object-oriented extension of Promela for the hierarchical modeling of structure and behaviour of concurrent reactive systems. Promela is a modeling language for concurrent, message based system and serves as the input language for the model checker Spin. The objective of this research is to reconcile Promela with state-of-the-art visual modeling techniques for real-time systems, in particular UML-RT, and to provide suitable tool support. VIP allows for the visual editing and maintenance of v-Promela models and provides a Promela code compiler. Later implementations will include result interpretation, support for dynamic capsule structures and object-oriented concepts at behaviour and structure level.

VIP is implemented in Java. We have shown a beta version at the 6th International Spin Workshop in Toulouse, France, on September 21, 1999. The tool is not generally publicly available, but if you wish to obtain a beta version, send an Email to Stefan.Leue "at" uni-konstanz.de.

Links to related resources

• Powerpoint presentation on VIP given at the 6th International Spin Workshop
• Moataz Kamel's Master's Thesis: On the Visual Modeling and Verification of Concurrent Systems
• Moataz Kamel's Master's Seminar: On the Visual Modeling and Validation of Concurrent Systems
• A paper describing the basic concepts of v-Promela: v-Promela: A Visual, Object-Oriented Language for Spin
• Resources on UML-RT (on ObjetTime's web site, there now called "UML for Real-Time")
• The Promela/Spin home page at Bell Labs