Skip to main content
Conference ProceedingsOPEN ACCESS

VIP: A visual editor and compiler for V-PROMELA

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2000) 1785 LNCS 471-486
DOI: 10.1007/3-540-46419-0_32
12Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

This article is free to access.

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. © Springer-Verlag Berlin Heidelberg 2000.

Cite

CITATION STYLE

APA

Kamel, M., & Leue, S. (2000). VIP: A visual editor and compiler for V-PROMELA. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1785 LNCS, pp. 471–486). Springer Verlag. https://doi.org/10.1007/3-540-46419-0_32

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free