Formal Methods, form09

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.