Print Email Facebook Twitter SPIN's Promela to Java Compiler: With help from Stratego Title SPIN's Promela to Java Compiler: With help from Stratego Author Vielvoije, E. Contributor Pronk, C. (mentor) Faculty Electrical Engineering, Mathematics and Computer Science Date 2008-09-23 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. Subject promelajavacompilerstratego To reference this document use: http://resolver.tudelft.nl/uuid:c7106f0b-5b8f-44fe-bca7-421653ec76c5 Publisher TU Delft, Electrical Engineering, Mathematics and Computer Science, Computer Science Part of collection Student theses Document type master thesis Rights (c) 2008 Vielvoije, E. Files PDF ewi_vielvoije_2008.pdf 1.28 MB Close viewer /islandora/object/uuid:c7106f0b-5b8f-44fe-bca7-421653ec76c5/datastream/OBJ/view