We are currently 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 using Sun's SDK 1.2. We have shown a beta version at the 6th International Spin Workshop in Toulouse, France, on September 21, 1999. The tool is not yet publicly available, but we expect a first public release later in the Fall of 1999. If you are interested in being notified of the availability of VIP, please send email to email@example.com.