SPIN's Promela to Java Compiler

With help from Stratego

Master thesis (2008)

Authors

Contributors

C. Pronk (mentor)
Faculty
Electrical Engineering, Mathematics and Computer Science (EEMCS) (TU Delft)
Copyright: © 2008 Vielvoije, E.
Java Compiler Promela Stratego
More Info
expand_more

Published Date

23-09-2008

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

In model checking a formal model of a software system is constructed. That model is verified against a set of properties expressed in some logic. Once a model has been created and verified, it is still necessary to write the application itself completely by hand. No tools have yet been developed that can automatically create a system or application using a model written in Promela. ... until now! The Promela2Java Compiler to be described in this paper is a unique tool transforming a Promela model into an executable Java application. The Promela2Java Compiler has been constructed using the Stratego/XT tool set. Developers can use SPIN to check their designs for certain properties and use the Promela2Java compiler to successfully create executable Java code from their designs.