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

Three hours per week

Modelling Reactive Systems (H)

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. 

Resit examinations ARE NOT ALLOWED for Honours students.

Resit examinations ARE ALLOWED for Masters students.

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. 

The course aims to encourage critical thinking and analysis of existing systems, tools and theories via research-based investigation.

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

1: Clearly differentiate issues that arise in concurrent, reactive, distributed systems, 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);

7: Critically evaluate existing techniques and methods.

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