The Theory of Concurrency in Real-Time Systems

The core of this course is a crash-course in CSP - Communicating Sequential Processes. This illustrates a branch of the theoretical/mathematical foundations underpinning computer science and yields a good understanding of the foundation of formal verification of software and design in addition to modeling of concurrent systems and the 'refinement' concept.

In addition there is project work, where synergies with the candidate's research project are strived for.

Knowledge:

• Thorough knowledge of CSP as a modelling language. (Basic syntax of CSP, events and processes Fundamental operators: prefixing, recursion, mu-recursion, alternation Parallel operators; alphabetized, interleaved, synchronous Channels and piping in CSP Sequential composition, termination, SKIP vs. STOP)
• Thorough understanding of divergence in CSP. (CSP hiding and renaming, and how hiding and renaming affects divergence)
• Thorough understanding of traces, failures and refinement.
• Thorough understanding the CSP definition of different types of refinement and how refinement can be used to check whether a process follows a specification.
• Knowledge of the general buffer process, and how this can be used to check correctness of communication protocols.

Skills:

• Be able to write models in machine-readable CSP for use with FDR3
• Be able to use FDR3 to check properties of systems defined in CSP.

General competence:

• Introduction to the process algebras
• Appreciating the theoretical foundation of computer science.
• Use of abstract mathematics

Lectures and project