University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Undergraduate Course: Communication and Concurrency (INFR11110)

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Credit level (Normal year taken)SCQF Level 11 (Year 4 Undergraduate) AvailabilityAvailable to all students
SCQF Credits10 ECTS Credits5
SummaryThe course provides an introduction to the Calculus of Communicating Systems (CCS) giving the theoretical foundation, examples of practical applications and logics for describing important properties. The course focuses on a mathematical model of the behaviour of concurrent systems which treats crucial notions like deadlock and non-determinism, and which reflects the modular construction of systems. The course also focuses on specifying safety and liveness properties of such systems. The approach is a mixture of operational semantics, algebra and logic. It applies alike to hardware and software. Although CCS is one of several alternative approaches, the aim is to treat it in depth rather than to make superficial comparisons with others.
Course description *Modelling communication: media, agents, ports;
*Basic definitions; synchronisation; action and transition; the basic calculus;
*Transitional semantics; derivatives and derivation trees;
*Bisimulation; modal and temporal logic;
*Strong bisimulation and strong equivalence; experimenting upon agents; observation equivalence; equality of agents;
*Communication protocols; specification of systems with evolving structure;
*Model checking.

Relevant QAA Computing Curriculum Sections: Concurrency and Parallelism; Distributed Computer Systems; Theoretical Computing; Programming Fundamentals
Entry Requirements (not applicable to Visiting Students)
Pre-requisites Co-requisites
Prohibited Combinations Other requirements This course is open to all Informatics students including those on joint degrees. For external students where this course is not listed in your DPT, please seek special permission from the course organiser.
Information for Visiting Students
Course Delivery Information
Not being delivered
Learning Outcomes
1 - Analyse computation, particularly concurrent systems in the process calculus CCS. The analysis consists of modelling situations by abstracting away from details and recording their fundamentals in a small computationally and mathematically appropriate formalism and then doing the same for their specifications. Finally one understands how to use all this to increase systems reliability.
2 - Define behaviour of a system as a transition graph.
3 - Understand when two systems are behaviourally equivalent. as defined by the notion of bisimulation equivalence.
4 - Verify that two systems are equivalent or prove that they are not.
5 - Specify temporal properties of systems in the branching time logic CTL.
6 - Understand the meaning of temporal formulas.
7 - Show that a system has, or fails to have, a temporal property.
8 - Use tools for systems verification.
9 - Be able to assimilate knowledge about different formalisms and tools and put them to practical use. Understanding how to apply mathematical and logical ideas in systems and other computational contexts.
Reading List
* ** R. Milner, Communication and Concurrency, Prentice-Hall 1989.
* ** C. Stirling, Modal and Temporal Properties of Processes, Springer Texts in Computer Science 2001.
* * C. Fencott, Formal Methods for Concurrency, International Thomson Computer Press 1996.
* * M. Hennessy, Algebraic Theory of Processes, MIT Press 1988
Additional Information
Course URL
Graduate Attributes and Skills Not entered
KeywordsNot entered
Course organiserDr Mary Cryan
Tel: (0131 6)50 5153
Course secretaryMiss Claire Edminson
Tel: (0131 6)51 4164
Help & Information
Search DPTs and Courses
Degree Programmes
Browse DPTs
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Combined Course Timetable
Important Information
© Copyright 2015 The University of Edinburgh - 18 January 2016 4:13 am