Module code: CO4209
All over the world, appliances using analog and mechanical parts are being phased out and replaced by CPUs and software. From everyday systems to critical software that is used in time-sensitive environments, we increasingly rely on the reliability of software to help us in our day to day tasks.
Here we will explore the verification tools and techniques required for assessing whether computer systems are reliable by seeing whether they have the qualifying properties. We will learn the limitations of these verification techniques (e.g. the state explosion problem) and the efforts to overcome them. We will discuss languages for modelling systems and their properties and use a selection of tools such as SPIN to verify and debug small-scale systems, whilst understanding the principles and algorithms behind these tools.
- 24 hours of lectures
- 16 hours of practicals/workshops
- 110 hours of guided independent study
- Coursework (40%)
- Exam, 2 hours (60%)