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.
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
- The Promela/Spin home page
Publications
- M. Kamel, S. Leue: VIP: A Visual Editor and Compiler for v-Promela, Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'2000, 2000. (PDF)
- Stefan Leue, Gerard Holzmann: v-Promela: A Visual, Object-Oriented Language for Spin, Proceedings of the Second IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, Saint Malo, France, IEEE Computer Society Press, 1999. (PDF)