# SYSTEMS VERIFICATION - 2023/4

Module code: COM3028

## Module Overview

The course is an introduction in formal methods for system specification and verification.

It will focus on logic-based formalisms and techniques, and specifically on model checking.

The main logics taught will be temporal logics, which are mainstream in verification, especially analysis of hardware systems.

Other logics and verification techniques (such as theorem proving) will be included to a smaller extended.

Model checkers will be used in the labs, on different system-verification problems.

Elements of building model checking tools will be presented and explored.

Some elements of advanced verification techniques (e.g., abstraction) will be mentioned.

### Module provider

Computer Science and Electronic Eng

### Module Leader

BOUREANU Ioana (CS & EE)

### Number of Credits: 15

### ECTS Credits: 7.5

### Framework: FHEQ Level 6

### JACs code: I100

### Module cap (Maximum number of students): N/A

## Overall student workload

Independent Learning Hours: 100

Lecture Hours: 11

Tutorial Hours: 10

Laboratory Hours: 8

Guided Learning: 10

Captured Content: 11

## Module Availability

Semester 2

## Prerequisites / Co-requisites

None

## Module content

The content (topics of lectures, tutorials and labs) follow:

1. Introduction + Introduction to System Verification

2. Basic Modal Concepts

**Tutorial **-- Modal specifications and satisfaction

3. The logics LTL and CTL

**Tutorial **-- LTL and CTL

4. The logics LTL vs CTL cont'd (expressivity) + The logic of CTL*

**Tutorial** -- LTL and CTL (cont’d)

5. Advanced Temporal Specifications Examples

**Lab ** -- on the introduction to a model checker

6. System-Modelling Examples

7. Hoare Logic

**Lab** -- Dafny

8. Explicit Model Checking

**Tutorial ** -- Explicit model checking

9. Binary Decision Diagrams (BDDs)

**Tutorial ** -- Binary Decision Diagrams

** Lab ** -- on using/manipulating BDDs

10. Symbolic Model Checking

**Lab ** -- on further, more advanced usage of a model checker

11. Non-classical Logics - Part I

12. Revision week

## Assessment pattern

Assessment type | Unit of assessment | Weighting |
---|---|---|

Coursework | COURSEWORK 1 | 15 |

Coursework | COURSEWORK 2 | 15 |

Examination | Exam (2h) | 70 |

## Alternative Assessment

N/A

## Assessment Strategy

The __assessment strategy__ is designed to provide students with the opportunity to demonstrate that they have achieved the module learning outcomes.

Thus, the __summative assessment__ for this module consists of:

· First individual coursework on temporal logic and explicit model checking. This addresses LO1 and LO2.

· Second individual coursework on applied non-classical logics, symbolic model checking of temporal logics and/or other verification techniques for applied logics (e.g., program verification with Hoare logic) . This addresses LO1 and LO2.

· A 2h unseen examination on the whole course content. This addresses LO1, LO2, LO3, LO4.

The individual pieces of coursework will be due around week 5 and 10 respectively. There will be five labs and the best four submissions of the total five will be considered towards the lab component of the mark. The exam will take place at the end of the semester during the exam period.

__Formative assessment and feedback__

1. PollEverywhere or other interactive polling methods will be used in the lectures with each lecture consisting of a number of slides explaining the theory followed by a number of slides gauging the students’ understanding. The answers are discussed when necessary, e.g., if a high proportion (more than 25%) of the students got the answer wrong.

2. Individual formative feedback will also be given during the lab sessions, and as part of the summative assessment.

## Module aims

- Introducing formal methods for system specification and verification
- Focus on logic-based techniques for system verification, particularly model checking
- Give a flavour of advanced model checking techniques and of other verification methods, such as theorem proving

## Learning outcomes

Attributes Developed | ||

001 | Understand the use of temporal logic and, to some extend, other logics as formal specification languages | KCT |

002 | Understand and use verification algorithms such as the ones based on SAT (satisfiability of logic formulae) and/or using ordered-binary-decision diagrams | KCPT |

003 | Learn how to use of a model checker and, potentially, a theorem prover to verify systems against formal specifications | KCP |

004 | Appreciate the limitations of current techniques and develop a basic understanding of research directions in this space | KC |

Attributes Developed

**C** - Cognitive/analytical

**K** - Subject knowledge

**T** - Transferable skills

**P** - Professional/Practical skills

## Methods of Teaching / Learning

The l__earning and teaching strategy__ is designed to develop a critical understanding of the foundations of systems verification, facilitating self-directed further studying in this field.

The skills learned in this module will be transferable to other verification techniques, such as program analysis.

Also developing critical thinking is at the core of this module.

The __learning and teaching method__s include:

- Lectures -- 11h (11 face-to-face flipped-lecture style lectures )
- Captured Content -- 11h (11h of recorded material, i.e., recorded presentations with the slides available)
- Tutorials -- 10h (5 theory-oriented tutorials at 2h each, preferably face-to-face)
- Labs -- 8h (4 practice-oriented labs at 2h each, preferably face-to-face)
- Guided learning -- 10h (tests and interaction on Surrey Learn)
- Independent Learning -- 100h (student study the material outside the settings above)

Indicated Lecture Hours (which may also include seminars, tutorials, workshops and other contact time) are approximate and may include in-class tests where one or more of these are an assessment on the module. In-class tests are scheduled/organised separately to taught content and will be published on to student personal timetables, where they apply to taken modules, as soon as they are finalised by central administration. This will usually be after the initial publication of the teaching timetable for the relevant semester.

## Reading list

https://readinglists.surrey.ac.uk

Upon accessing the reading list, please search for the module using the module code: **COM3028**

## Other information

**Digital Capabilities**

This module teaches student the theory and practical skills to reason about the correctness of computer programs. The module builds on earlier technical modules such as COM1026 (Foundations of Computing) to provide students with a way model a program mathematically and tools to assess its correctness. These are digital skills that are highly valued in some industries where safety critical systems rely on the correctness of a computer program.

**Employability**

This module provides foundational theory to reason about correctness of computer systems and programs which is highly valued and, in the last decade, often used in industry. In particular, this is of paramount importance to industries that work with safety-critical systems, e.g., aviation, automotive, satellite. Students are equipped with theoretical and practical problem-solving skills, and transferable mathematical and theoretical computer-science knowledge that allow them to analysis in theory and in practice (via tools) the formal correctness of complex systems of various types, e.g., high-level designs, software, communication protocols. All of this is highly valuable to employers for different roles: system architects, software developers, testers.

**Global and Cultural Skills**

Computer Science is a global language and the tools and languages used on this module can be used internationally. This module allows students to develop skills that will allow them to develop applications with global reach and collaborate with their peers around the world.

**Resourcefulness and Resilience**

This module involves practical problem-solving skills that teach a student how to reason about and solve new unseen problems through combining the foundation theory taught with practical technologies for systems that are in everyday use. Students will have exposure to new tools that will allow them to approach this complex problem of correctness in a new way.

## Programmes this module appears in

Programme | Semester | Classification | Qualifying conditions |
---|---|---|---|

Computing and Information Technology BSc (Hons) | 2 | Optional | A weighted aggregate mark of 40% is required to pass the module |

Computer Science BSc (Hons) | 2 | Optional | A weighted aggregate mark of 40% is required to pass the module |

Computer Science MEng | 2 | Optional | A weighted aggregate mark of 40% is required to pass the module |

Please note that the information detailed within this record is accurate at the time of publishing and may be subject to change. This record contains information for the most up to date version of the programme / module for the 2023/4 academic year.