Course content

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.

Learning outcome

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

Learning methods and activities

Lectures and project

Compulsory assignments

• Exercises

Recommended previous knowledge

Knowledge corresponding to TTK4145 Real-Time programming is recommended.

Course materials

A.W. Roscoe: The Theory and Practice of Concurrency. Other litterature may be announced at the start of the semester.