Distributed Systems Programming F29NM1:
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.
Lecture material:
- Formal Methods for System Design [
ps
pdf ]
- Formal Verification [
ps
pdf ]
- Promela I [
ps
pdf ]
- Promela II [
ps
pdf ]
- SPIN: Simple Promela INterpreter [
ps
pdf ]
- SPIN: Formal Analysis I [
ps
pdf ]
- SPIN: Formal Analysis II [
ps
pdf ]
- LTL Reasoning: How It Works [
ps
pdf
]
[ extra material ]
- Formal Methods for Distributed Systems: Summary [
ps
pdf ]
Laboratory material:
Tool support:
- XSPIN (graphical version of SPIN) is available under
Linux within the School, simply type xspin at
the prompt.
Web based Tutorial (Flash):
Assignment 2007/2008:
-
An exercise in distributed system modelling and verification
[
ps
pdf
]
- Results for 2007/2008 are available
here
Recommended reading:
- 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
-
Basic Spin Manual
Recommended Web links: