THE UNIVERSITY of EDINBURGH

DEGREE REGULATIONS & PROGRAMMES OF STUDY 2011/2012

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

Undergraduate Course: Communication and Concurrency (INFR10007)

Course Outline
School School of Informatics College College of Science and Engineering
Course type Standard Availability Available to all students
Credit level (Normal year taken) SCQF Level 10 (Year 4 Undergraduate) Credits 10
Home subject area Informatics Other subject area None
Course website http://www.inf.ed.ac.uk/teaching/courses/coc Taught in Gaelic? No
Course description The 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.
Entry Requirements
Pre-requisites It is RECOMMENDED that students have passed Language Semantics and Implementation (INFR09014)
Co-requisites
Prohibited Combinations Other requirements Successful completion of Year 3 of an Informatics Single or Combined Honours Degree, or equivalent by permission of the School. There are no formal prerequisites although the Language Semantics & Implementation course is particularly relevant. The course requires a reasonable mathematical ability.
Additional Costs None
Information for Visiting Students
Pre-requisites None
Displayed in Visiting Students Prospectus? Yes
Course Delivery Information
Delivery period: 2011/12 Semester 1, Available to all students (SV1) WebCT enabled:  No Quota:  None
Location Activity Description Weeks Monday Tuesday Wednesday Thursday Friday
CentralLecture1-11 14:00 - 14:50
CentralLecture1-11 14:00 - 14:50
First Class First class information not currently available
Exam Information
Exam Diet Paper Name Hours:Minutes
Main Exam Diet S2 (April/May)2:00
Delivery period: 2011/12 Semester 1, Part-year visiting students only (VV1) WebCT enabled:  No Quota:  None
Location Activity Description Weeks Monday Tuesday Wednesday Thursday Friday
CentralLecture1-11 14:00 - 14:50
CentralLecture1-11 14:00 - 14:50
First Class First class information not currently available
Exam Information
Exam Diet Paper Name Hours:Minutes
Main Exam Diet S1 (December)2:00
Summary of Intended 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.
Assessment Information
Written Examination 70
Assessed Assignments 30
Oral Presentations 0

Assessment

Two submissions are required, equally weighted. The first involves extensive use of the Concurrency Workbench. The second tests understanding (e.g., of bisimulation); it is a mixture of exercises, and questions similar to those that may occur in exams.

If delivered in semester 1, this course will have an option for semester 1 only visiting undergraduate students, providing assessment prior to the end of the calendar year.
Special Arrangements
None
Additional Information
Academic description Not entered
Syllabus *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
Transferable skills Not entered
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
Study Abroad Not entered
Study Pattern Lectures 20
Tutorials 0
Timetabled Laboratories 0
Non-timetabled assessed assignments 30
Private Study/Other 50
Total 100
Keywords Not entered
Contacts
Course organiser Dr Amos Storkey
Tel: (0131 6)51 1208
Email: A.Storkey@ed.ac.uk
Course secretary Miss Kate Weston
Tel: (0131 6)50 2701
Email: Kate.Weston@ed.ac.uk
Navigation
Help & Information
Home
Introduction
Glossary
Search DPTs and Courses
Regulations
Regulations
Degree Programmes
Introduction
Browse DPTs
Courses
Introduction
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Timetab
Prospectuses
Important Information
 
copyright 2011 The University of Edinburgh - 3 April 2011 11:20 am