30 credits – Automated Deductive Verification of Embedded C Code

Thesis project at Scania is an excellent way of making contacts for your future working life. Many of our current employees started their career with a thesis project.

Background
A significant part of the code base of the embedded systems developed at Scania is written in the C programming language. The systems controlled by such code are often of a safety-critical nature and are expected to comply to safety standards such as ISO 26262.  As part of the overall safety requirements, the correctness of the embedded C code is of paramount importance.

The present project focuses on the functional correctness of C code. As opposed to debugging, which aims at detecting and eliminating potential runtime errors, functional correctness of a given piece of code refers (in the present context) to the correct transformation of data when executing the code. Such correctness is always relative to a specification that describes the intended function of the code.

The activity of establishing the functional correctness of code by formal means is usually called program verification. The specifications are typically written in a logic notation and are provided as annotations to the program to be verified [1]. Technically, program verification is usually based on Hoare logic and uses symbolic execution or weakest precondition generation to produce verification conditions, combined with automated theorem proving for discharging these. Various tools of academic and industrial origin and of various degrees of maturity and usability are available to support functional verification. For the C programming language, well-known tools include VCC [2] and Frama-C [3].

In a previous project at Scania, VCC was selected and used to verify a number of functional requirements of a given C module, starting from a semi-formal description of the requirements in an internal document. The project resulted in the formulation of a formal requirements model, a formalization of the requirements in term of this model, and an annotation of the code base. While the project demonstrated the applicability of deductive verification to functional requirements of a real module, it required significant effort in terms of time and expertise. The present project aims at automating the annotation process as much as possible, in order to potentially integrate verification as part of the code development and maintenance process at Scania.

Tasks
The present project involves the following tasks:
Getting familiar with the code base, its safety requirements, and the VCC tool.
Studying the results of the previous project: the requirements model, the formalization of the requirements, and the code annotation.
Development of an approach to automating the annotation process.
Implementation of the approach and evaluation on a concrete module.
Writing up the results and conclusions in a report (Master’s thesis).

Required Outcomes
The required outcomes of this project are:
An approach to automating the annotation process.
An implementation of the approach and evaluation on a concrete module.
A Master’s thesis that documents all results and conclusions.

Initial Reading Material
[1] Michael Huth, Mark Ryan: Logic in Computer Science, Cambridge University Press
2004 (2nd edition), ISBN 0 521 54310X.

[2] Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal,
Thomas Santen, Wolfram Schulte, Stephan Tobies: VCC: A Practical System for
Verifying Concurrent C. Conference on Theorem Proving in Higher
Order Logics (TPHOLs 2009). LNCS 5674. 2009.

[3] Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles,
Boris Yakobowski: Frama-C: A Software Analysis Perspective. International
Conference on Software Engineering and Formal Methods, LNCS 7504, pp 233-247.
2012.

Education
Computer science, C programming, mathematical logic, formal methods (optional).

Number of students: 1-2
Estimation of time needed: 20 weeks

Contact Person
Dilian Gurov, tel 08-790 81 98, email: dilian@csc.kth.se

Application
Please include the university grades in your application. Note that students from all universities (and not just KTH) are eligible.

About the job

  • Title: 30 credits – Automated Deductive Verification of Embedded C Code
  • Business area: Thesis work
  • Country: Sweden
  • City: Sodertalje
  • Last application date: 2017-09-01
  • Job Id: 20164368