TTK3 - An introduction to formal verification

Teacher: Sverre Hendseth

Formal verification of software is on the rise for more reasons.

1. The theory, practices and tools are maturing (slowly).
2. Awareness of software quality has been high for more decades acknowledging that testing and adherence to development methodologies are insufficient. As formal verification becomes steadily more available it is taken into the expectations of quality software.
3. The definition of safety critical software is rapidly expanding. It is not only nuclear power plants and airplanes any more, but the fire alarm systems of Autronica here in Trondheim, lots of your cars subsystems, any moving system, any system physically interacting with a human, the controller of your kitchen stove? Etc. Etc.

You will likely encounter the formal verification requirement during your career. The purpose of this module is to build some intuition on what this entails.

Going through this module you will:

1. when confronted with a tool or method for formal verification, be able to put it into context of how it works, usefulness and limitations.
2. see that some aspects of computer science is not just ad-hoc, «what works» engineering, but can be appreciated as a science. (This is good for you.)

Curriculum will be the open book Theory and Practice of Concurrency by Roscoe. We aim at a reasonable understanding of the concept of Refinement. If you can appreciate example 5.1.1 on page 120 in the book you are well set for the exam (but see under for alternative route for passing the course).

The book introduces a branch of mathematics concerning «Communicating Sequential Processes» (CSP) and is quite theoretical (lots of axioms, operators, theorems etc.).

Sverre will cover this theory in 7×2 hour lectures.

You are encouraged to choose this route.

1. Look for how formal verification can be applied in, or be relevant for your project work this autumn. Explore this, and present it for the class, me and sensor.
2. Find a tool, theory or method for formal verification that sparks your interest. Explore&present.

The oral exam will then not be centered around the Roscoe theory, but on your study/ your results. (We will discuss the timing… If bureaucracy allows, and you want, we will grade you then and there after your presentation.)

For those choosing the alternative route, the 7×2 lectures are mandatory.

If not doing the alternative route I also … very strongly encourage you to model the «hard to find bug» (a 20 line semaphore program from TTK4145 and the Burns and Wellings «Real-Time Systems and Programming Languages» book) in either FSP/LTSA or FDR3, just to ensure that you are not taking too lightly on the theory.