Distributed Systems Programming F21DS1:
Formal Methods for Distributed Systems
Aims and objectives:
To promote an understanding of the issues involved in using formal methods
within system design, in particular the design of distributed and concurrent
systems; To provide practical experience of the formal modelling and analysis
of such systems through the SPIN design verification tool; To give an insight
into the theory which underpins such formal modelling and analysis tools.
- Formal Methods for System Design [
- Formal Verification [
- Promela I [
- Promela II [
- SPIN: Simple Promela INterpreter [
- SPIN: Formal Analysis I [
- SPIN: Formal Analysis II [
- LTL Reasoning: How It Works [
- Formal Methods for Distributed Systems: Summary [
- XSPIN (graphical version of SPIN) is available under
Linux within the School, simply type xspin at
Web based Tutorial (Flash):
An exercise in distributed system modelling and verification [ available ]
- Holzmann, G.J. "The Spin Model Checker - Primer and Reference Manual".
The new book, describing the most recent version of Spin,
Addison-Wesley Publ., ISBN 0-321-22862-6, available September 2003.
- Holzmann, G.J. "Design and Validation of Computer Protocols",
Prentice Hall, 1991. The first Spin book. Spin was written for
this book in 1989.
- Holzmann, G.J. "The Model Checker SPIN",
IEEE Transactions on Software Engineering, Vol 23 (5), 1997.
Formal Methods Specification and Analysis Guidebook for the Verification
of Software and Computer Systems,
Volume II: A Practitioner's Companion [NASA-GB-001-97], 1997
Recommended Web links: