Visual Modeling and Formal
This presents a collection of papers pertaining to the v-Promela
notation and the VIP (Visual Interface for Promela) tool. More
information on VIP can be obtained from the VIP
home page (under construction).
VIP: A Visual Editor and Compiler
M. Kamel and S. Leue
S. Graf and M. Schwartzbach (eds.), Proceedings of the 6th
International Conference on Tools and Algorithms for the Construction
and Analysis of Systems TACAS'2000, Lecture Notes in Computer Science,
p. 471 - 486, Springer Verlag, March 2000.
We describe the Visual Interface to Promela (VIP) tool that
we have recently implemented. VIP supports the visual editing and
maintenance of v-Promela models. v-Promela is a visual, object-oriented
extension to Promela, the input language to the Spin~model checker.
We introduce the v-Promela notation as supported by the VIP editor,
discuss Promela code generation, and describe the process of property
validation for the resulting models. Our discussion centers around
two case studies, a call processing system and the CORBA GIOP protocol.
v-Promela: A Visual, Object-Oriented
Language for Spin
Stefan Leue and Gerard Holzmann
To appear in:
Proceedings of the Second IEEE International Symposium on Object-Oriented
Real-Time Distributed Computing, 3rd.-5th. May 1999, Saint Malo, France,
IEEE Computer Society Press, 1999.
We describe the design of VIP, a graphical front-end to the
model checker Spin. VIP supports a visual formalism, called v-Promela
that connects the model checker to modern hierarchical notations for
the specification of object-oriented, reactive systems. The formalism
is comparable to formalisms such as UML-RT, ROOM, and Statecharts, but
is presented here in a framework that allows us to combine the benefits
of a visual, hierarchical specification method with the power of LTL
model checking provided by Spin. Like comparable formalisms, VIP can
describe hierarchies of behaviour and of system structure. The formalism
is designed to be transparent to the Spin model checker itself, by allowing
all central constructs to be translated mechanically into basic Promela,
as already supported by the existing model checker.