publication . Part of book or chapter of book . Conference object . 2001

VIP: A Visual Editor and Compiler for v-Promela

Kamel, Moataz; Leue, Stefan;
Open Access
  • Published: 01 Jun 2001
  • Publisher: Springer Berlin Heidelberg
  • Country: Germany
Abstract
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.
Subjects
free text keywords: Compiler, computer.software_genre, computer, Theoretical computer science, Common Object Request Broker Architecture, SPIN model checker, Promela, computer.programming_language, Computer science, Programming language, Visual programming language, Formal verification, Code generation, Formal specification, ddc:004
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Part of book or chapter of book . Conference object . 2001

VIP: A Visual Editor and Compiler for v-Promela

Kamel, Moataz; Leue, Stefan;