Advanced Concurrency Tools: Model Checking

The rigorous development of a complex concurrent or distributed system is an immense challenge for any organisation. This course teaches principles of structure and refinement that are particularly useful in understanding such systems. An essential feature of this course is the comprehensive tool support that is provided for reasoning about concurrent systems: communications protocols, distributed databases, and control systems.

Course dates

Objectives

Students will gain experience in applying the Communicating Sequential Processes (CSP) formalism to realistic problems in specification and design. They will also gain experience in using a practical toolset for refinement testing and analysis.

Contents

CSP:

process syntax; events; abstraction; refinement.

Observations:

execution; history; testing; deadlock; livelock.

Model-checking:

tools; principles; context.

Protocols:

: modelling and analysis; errors; media specification.

Control systems:

interaction; failure; interference.

Combinatorics:

transition systems; modelling large systems.

Time:

timing constraints; timeouts; delays.

Non-interference:

security; safety; fault-tolerance.

Dealing with state explosion:

data-independence; compression strategies.

Requirements

Students will be expected to have a working knowledge of the CSP notation: Concurrency and distributed systems would be an ideal preparation. Any student who has not taken Concurrency and distributed systems should ask for advice before registering for this course.