Modelling Reactive Systems (M) COMPSCI5075
- Academic Session: 2021-22
- School: School of Computing Science
- Credits: 10
- Level: Level 5 (SCQF level 11)
- Typically Offered: Semester 2
- Available to Visiting Students: No
- Available to Erasmus Students: No
Modelling concurrent, communicating systems using non-probabilistic and probabilistic techniques, verification using the SPIN and PRISM model checkers, and specification and strategy synthesis for reactive systems using inductive and probabilistic techniques.
Three hours per week
Requirements of Entry
Algorithmic Foundations 2 (or equivalent).
Modelling Reactive Systems (H)
Examination (80%); practical exercise (20%)
Main Assessment In: April/May
Are reassessment opportunities available for all summative assessments? No
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. Lastly, students will learn about model synthesis from specifications, combining inductive learning and deduction, specification inference, game-theoretic approaches in the PRISM, and find out about emerging applications in the area including formal methods for safe AI.
The course aims to encourage critical thinking and analysis of existing systems, tools and theories via research-based investigation.
Intended Learning Outcomes of Course
By the end of this course students will be able to:
1: Clearly differentiate issues that arise in concurrent, reactive, and distributed 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: Explain concepts and applications of formal methods for synthesis from specifications or execution traces;
8: Critically evaluate existing techniques and methods.
Minimum Requirement for Award of Credits
Students must submit at least 75% by weight of the components (including examinations) of the course's summative assessment.