Skolan för
och kommunikation
KTH / CSC / Kurser / DD2452 / form09 / Tools

Formal Methods, form09

DD2452 Formal Methods: Tools


  1. ESC/Java2. Please refer to the ESC/Java2 Implementation Notes and the ESC/Java User's Manual for examples and for a detailed explanation of the features of the tool (we shall use the overview and the first example from the manual as a tutorial; here is the source code for Bags in Java, and here is an annotated version). The following paper provides a good overview of the (first version of the) tool and its use.
  2. The Spin Model Checker (installation instructions). To get aquainted with Promela and SPIN,  you are recommended to do the Introductory Promela Exercises; here is the Promela code for the Alternating Bit Protocol. For a full description of the tool and its list of commands please refer to the SPIN User's Manual. Have a look also at the Concise Promela Reference by Rob Gerth. For the theoretical foundations of SPIN, please consult the book Design and Validation of Computer Protocols by Gerard Holtzmann. The following paper by the same author provides a good overview of the (first version of the) tool and its use.
To run ESC/Java2 and SPIN on our (CSC) computers, add modules escjava and spin and execute escjava2 and xspin, respectively.

Copyright © Sidansvarig: Dilian Gurov <>
Uppdaterad 2009-01-12