Software reliability methods are now past the stage of "promising
curiosities" and offer techniques and tools that can be employed in
a variety of application domains to verify required functional
properties against models of system behaviour.
This module covers some of these techniques and tools, namely those
which, like SPIN, are based on model-checking. It introduces
students to languages for modelling systems and their properties,
some of the algorithms that can be employed for automatic
verification, and the limitations of current implementations.
