CS4052: Logic and Software Verification
This module is offered in 2022-23.
Aims
The aims of this module are:
- To introduce the idea and motivation behind formal methods in general and model checking in particular.
- To introduce the idea of program semantics and verification.
Learning Outcomes
On successful completion of this module, the student should:
- Be aware of the need for formal methods and software verification.
- Be familiar with a variety of well known model checkers.
- Have a working knowledge of relevant approaches to modelling and property specification.
- Understand the fundamental principles underlying model checking.
- Be able to use transition systems as a model for systems, and temporal logics to express system properties including functional correctness, reachability, safety, liveness, fairness and real-time properties.
- Be able to specify and verify models using various approaches including PROMELA and SPIN, timed Automata and UPPAAL (real-time systems), and Petri nets.
Syllabus
- Modelling concurrent systems: transition systems, program graphs, parallelism and communication.
- Linear-time properties: deadlock, safety, liveness, fairness contraints.
- Temporal logics: LTL and CTL.
- Model checking with PROMELA and SPIN.
- Model checking with Timed Automata and UPPAAL.
- Petri nets.
- Program verification.
Compulsory Elements
This module has no compulsory elements beyond those common to all modules (mark of 4 in each assessment component).