Specification and Verification of Concurrent Systems
Designing concurrent systems that behave correctly is inherently difficult: a linear increase in the number of components leads to an exponential increase in the number of potential interactions to consider. This inherent complexity means that ad hoc analyses are insufficient for ensuring that a system's behavior is correct. It is therefore essential to have sound mathematical bases for specifying what consitutes correct behavior and for verifying that the resulting design satsifies this specification.
Many formalisms have been introduced for the specification and verification of concurrent systems. In this course, we will focus on the process-algebraic approach: we will use the process algebra CSP to model concurrent systems, and we will use an industrial-strength, computer-based tool (FDR) to analyze the behavior of such systems. The course will involve regular assignments and (depending on class size) either a final project/presentation or two in-class exams.