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 (mandatory), 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. Apply directly to Dilian Gurov.

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: 2018-01-31
  • Job Id: 20164368

About Scania

Scania ingår i Volkswagen Truck & Bus GmbH och är en av världens ledande tillverkare av lastbilar och bussar för tunga transporter samt industri- och marinmotorer. En växande del av verksamheten är service- och tjänsteutbudet, som garanterar Scanias kunder kostnadseffektiva transportlösningar och hög tillgänglighet. Scania erbjuder också finansiella tjänster. Scania är verksamt i ett hundratal länder och har 44 000 anställda. Forskning och utveckling är koncentrerad till Sverige. Tillverkning sker i Europa och Sydamerika med möjlighet till globalt utbyte av såväl komponenter som kompletta fordon. Under 2015 uppgick faktureringen till 95 miljarder kronor och resultatet efter skatt till 6,8 miljarder kronor Scanias pressreleaser finns på www.scania.com/group