SYSTEMS VERIFICATION - 2020/1

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

Module Leader

BOUREANU Ioana (Computer Sci)

Number of Credits: 15

ECTS Credits: 7.5

Framework: FHEQ Level 6

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

Module Availability

Semester 2

Prerequisites / Co-requisites

Basic discrete maths (sets, functions, etc.) -- COM1026 Basic propositional calculus --  COM1026 Basic first-order logic  -- COM1026 Basic C/C++ programming -- COM2040  

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 3 -- LTL and CTL (cont’d)

5.  Advanced Temporal Specifications Examples

     Lab  -- on the introduction to a model checker

6.  System-Modelling Examples

7.  Explicit Model Checking

     Tutorial  -- Explicit model checking

8.  Binary Decision Diagrams (BDDs)

     Tutorial  -- Binary Decision Diagrams

     Lab  -- on using/manipulating BDDs

9. Symbolic Model Checking

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

10. Non-classical Logics - Part I

11. Non-classical Logics - Part II

12. Revision week

Assessment pattern

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. 

----------

Assessment & Assessment Strategy:  Executive Summary

Coursework 1 (15%) -- take-home work, testing learning outcomes 1 and 2

Coursework 2  (15%) -- take-home work, testing learning outcomes 1 and 2

Final exam (70%) --  unseen written piece of examination in the exam period, testing learning outcomes 1, 2, 3 and 4

 

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

Methods of Teaching / Learning

The learning 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 methods include:

• Twenty-four hours of lectures with class discussion


• Ten hours of tutorials


• Six hours of lab classes


• Use of an online forum for facilitated discussion

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

REFERENCES:

1. Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York, NY, USA.
2. Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics: With Isabelle/HOL. Springer Publishing Company.
3. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. 2003. Reasoning about Knowledge. MIT Press, Cambridge, MA, USA.

Programmes this module appears in

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 2020/1 academic year.