course-details-portlet

TK8112 - The Theory of Concurrency in Real-Time Systems

About

Examination arrangement

Examination arrangement: Oral examination
Grade: Passed/Failed

Evaluation Weighting Duration Grade deviation Examination aids
Oral examination 100/100

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

Specific conditions

Compulsory activities from previous semester may be approved by the department.

Course materials

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

More on the course

No

Facts

Version: 1
Credits:  7.5 SP
Study level: Doctoral degree level

Coursework

Term no.: 1
Teaching semester:  AUTUMN 2021

Language of instruction: English

Location: Trondheim

Subject area(s)
  • Computer and Information Science
  • Engineering Cybernetics
Contact information
Course coordinator: Lecturer(s):

Department with academic responsibility
Department of Engineering Cybernetics

Examination

Examination arrangement: Oral examination

Term Status code Evaluation Weighting Examination aids Date Time Examination system Room *
Autumn ORD Oral examination 100/100
Room Building Number of candidates
Spring ORD Oral examination 100/100
Room Building Number of candidates
  • * The location (room) for a written examination is published 3 days before examination date. If more than one room is listed, you will find your room at Studentweb.
Examination

For more information regarding registration for examination and examination procedures, see "Innsida - Exams"

More on examinations at NTNU