Undergraduate Course: Formal Verification (INFR11129)
Course Outline
| School | School of Informatics |
College | College of Science and Engineering |
| Credit level (Normal year taken) | SCQF Level 11 (Year 4 Undergraduate) |
Availability | Available to all students |
| SCQF Credits | 10 |
ECTS Credits | 5 |
| Summary | Formal verification is the use of mathematical techniques to verify the correctness of various kinds of engineering systems: software systems and digital hardware systems, for example. Formal verification techniques are exhaustive and provide much stronger guarantees of correctness than testing or simulation-based approaches. They are particularly useful for safety and security critical systems and for when system behaviour is highly complex. The course focuses on automated techniques that are currently used in industry. It gives practical exposure to current formal verification tools, explaining the input languages used and introducing the underlying mathematical techniques and algorithms used for automation. |
| Course description |
In recent years there have been highly noteworthy cases of the adoption of formal verification (FV) techniques in industry. For example, at Intel, FV has largely replaced simulation-based verification of their microprocessors, at Microsoft, FV is used to certify that 3rd party drivers are free of certain kinds of concurrency bugs. As FV tools and methodologies improve, FV is expected to become more and more widely used in industry.
This course aims to familiarise students with main classes of FV techniques that are likely to become most widespread in industry in the coming years. The intent is to prepare students who might go into industry with sufficient background in FV that they would be aware of when and how they might deploy FV techniques. The course will also be of interest to students who wish to go into research developing techniques for future-generation FV tools and who might need to use FV in their research. To satisfy these aims, the course has a practical focus, giving students hands-on experience with a number of tools and explaining their input languages for specifying systems and desired system properties. The course also introduces the underlying mathematical techniques, which gives students a deeper understanding of the tools and will help them use the tools most effectively.
Topics the course covers include the following:
*Formal verification in context, its current take-up in industry and challenges to its wider
adoption
*Syntax and semantics of CTL and LTL temporal logics
*CTL and LTL model checking techniques, including automata-based approaches and
bounded model checking with SAT solvers
*The BDD data-structure used at the heart of many model checkers
*Writing models for model checking and phrasing useful properties in CTL and LTL
*Operational semantics of a simple imperative programming language, weakest precondition
operators and verification condition generation
*The capabilities of SMT solvers for discharging verification conditions
*Assertion-based software verification
*Software model checking, focusing on its use for finding concurrency bugs
*Pattern-based detection of concurrency bugs
Optional topics include:
*Industrial temporal logics such as PSL and SVA used in hardware verification
*Formal verification case studies
*Formal verification of hybrid systems, system with both discrete state changes and
continuous state changes governed by differential equations
*Combining formal and simulation-based verification methods
*Dual use of temporal logic properties and assertions in formal and simulation-based
verification of hardware and software
|
Entry Requirements (not applicable to Visiting Students)
| Pre-requisites |
|
Co-requisites | |
| Prohibited Combinations | |
Other requirements | Incoming students are expected to be familiar with discrete maths at a level similar to that taught in the School of Informatics course Discrete Mathematics and Mathematical Reasoning (INFR08023). Prior exposure to predicate logic is also helpful. Programming experience in an imperative language such as Java, C or C++ is also essential for handling the material related to software verification.
For the hardware verification aspects of the course, prior exposure to hardware design is not needed, but students do need to be familiar with Finite-State Automata concepts. |
Information for Visiting Students
| Pre-requisites | See above. |
| High Demand Course? |
Yes |
Course Delivery Information
|
| Academic year 2017/18, Available to all students (SV1)
|
Quota: None |
| Course Start |
Semester 2 |
Timetable |
Timetable |
| Learning and Teaching activities (Further Info) |
Total Hours:
100
(
Lecture Hours 17,
Supervised Practical/Workshop/Studio Hours 10,
Feedback/Feedforward Hours 4,
Summative Assessment Hours 2,
Programme Level Learning and Teaching Hours 2,
Directed Learning and Independent Learning Hours
65 )
|
| Assessment (Further Info) |
Written Exam
100 %,
Coursework
0 %,
Practical Exam
0 %
|
| Additional Information (Assessment) |
Written Examination: 100%
The course material is primarily introduced in lectures and assessment is by a final exam. Practical exercises are provided to give students familiarity with formal verification tools and help them better understand formal verification techniques. Support for students in using the tools is provided both by demonstrators in lab sessions and through the use of an online discussion forum. In addition, demonstrators review student solutions to exercises and the lecturer both introduces the exercises and presents model solutions.
As the course focuses on the application of formal verification techniques, most exam questions will involve presenting various verification scenarios and exploring how verification techniques might be deployed in those scenarios. Often questions will focus on some particular aspect of a techniques, exploring for example how well students understand the input specification languages used by techniques. Other questions might involve students stepping through the behaviour of verification algorithms on small examples.
|
| Feedback |
An online discussion forum will provide one channel for feedback on all aspects of the course, including replies to questions concerning lectures, practical exercises and previous
exams.
Lectures will include feedforward introductory presentations on the practical exercises and walkthroughs and discussion of model answers to the exercises.
Demonstrators in labs will be available for providing feedback on students work on the practical exercises on a as-needed basis. In addition, students will be able to book slots, maybe 15 mins in length, during which a demonstrator can systematically walk through students work and compare it with model solutions.
We will consider recommending students work in pairs on the exercises, so they have the benefit of peer feedback. Students could also meet with demonstrators in these pairs, which would enable demonstrator resources to be stretched further and possibly could enable longer demonstrator meeting times. |
| Exam Information |
| Exam Diet |
Paper Name |
Hours & Minutes |
|
| Main Exam Diet S2 (April/May) | | 2:00 | |
Learning Outcomes
On completion of this course, the student will be able to:
- Deploy bounded and unbounded model checking techniques to formally verify temporal logic properties of digital hardware and other finite state systems and protocols,
- Use an assertion-based software formal-verification tool to verify desired properties of computer programs,
- Describe formal techniques that can be used for the detection of concurrency bugs in software,
- Assess the pros and cons of using different automated formal verification approaches on a previously-unseen hardware or software system.
|
Reading List
- Logic in Computer Science (2nd Ed).why3 Huth and Ryan. Cambridge UP. 2004.
- NuSMV model checker documentation and tutorials. http://nusmv.fbk.eu/
- SPARK toolset documentation and training materials. Altran UK. 2016. Overview at http://intelligent-systems.altran.com/technologies/software-engineering/spark.html
Training materials accessed via SPARK Academic Programme.
- Why3 programme verification toolkit documentation and tutorials. http://why3.lri.fr
- CBMC (Bounded model checker for C and C++) documentation, http://www.cprover.org/cbmc/. |
Additional Information
| Graduate Attributes and Skills |
- Apply critical analysis, evaluation and synthesis to forefront issues, or issues that are informed by forefront developments in the subject/discipline/sector.
- Critically review, consolidate and extend knowledge, skills, practices and thinking in a subject/discipline/sector.
- Deal with complex issues and make informed judgements in situations in the absence of complete or consistent data/information.
- Communicate with peers, more senior colleagues and specialists.
- Use a wide range of ICT applications to support and enhance work at this level and adjust features to suit purpose. |
| Keywords | Hardware verification,Formal verification,Software verification,Model checking,SMT,SAT,BDD,Assertion |
Contacts
| Course organiser | Dr Paul Jackson
Tel: (0131 6)50 5131
Email: |
Course secretary | Mr Gregor Hall
Tel: (0131 6)50 5194
Email: |
|
|
University Homepage