Course Catalogue

View Specification Document | Reading List

Modelling concurrent, communicating systems using non-probabilistic and probabilistic techniques, verification using the SPIN and PRISM model checkers.

Three hours per week

Algorithmic Foundations 2 (or equivalent).

Modelling Reactive Systems (M)

None

Examination (80%); practical exercise (20%)

Reassessments are normally available for all courses, except those which contribute to the Honours classification. For non Honours courses, students are offered reassessment in all or any of the components of assessment if the satisfactory (threshold) grade for the overall course is not achieved at the first attempt. This is normally grade D3 for undergraduate students and grade C3 for postgraduate students. Exceptionally it may not be possible to offer reassessment of some coursework items, in which case the mark achieved at the first attempt will be counted towards the final course grade. Any such exceptions for this course are described below. 

The coursework cannot be redone because the feedback provided to the students after the original coursework would give any student redoing the coursework an unfair advantage.

Reactive systems are widely and increasingly used throughout society (e.g. telecommunications, flight control, railway signalling, medical devices). An understanding of the fundamentals of these systems, at an abstract level, is essential for the development of process control systems and should be a pre-requisite for anyone developing software for such applications. This course provides in-depth study of key formal techniques used in designing and analysing concurrent, reactive systems; and to present the practical issues raised by using a number of such formalisms and associated software tools, particularly within the context of developing communications protocols and other communications applications. 

Students will learn to model systems using the Promela specification language and associated verification tool SPIN. In addition, probabilistic systems will be modelled as Discrete Time Markov Chains using the PRISM language and tool.

By the end of the course students will be able to:

1: Clearly differentiate issues that arise in concurrent, reactive, distributed, and probabilistic systems;

2: Explain the various concepts of concurrency and communication that arise in such systems;

3: Demonstrate understanding of the concepts of signalling and control and associated modelling issues;

4: Develop message sequence charts for a reactive system;

5: Enumerate the differences between non-probabilistic and probabilistic formalisms;

6: Design and analyse a reactive system, including a communication protocol, using appropriate design techniques and mechanised analysis tools (SPIN and PRISM);

Students must submit at least 75% by weight of the components (including examinations) of the course's summative assessment.