PhD Defence Philip Ben Heinrich Tasche | Deductive Verification Techniques for Embedded Systems

Deductive Verification Techniques for Embedded Systems

Philip Ben Heinrich Tasche is a PhD student in the Department of Formal Methods and Tools. Promotors are prof.dr. M. Huisman and prof.dr.ing. P. Herber from the Faculty of Electrical Engineering, Mathematics and Computer Science.

From planes to power plants, embedded systems are controlling vital functions of our society. 99% of all globally produced microcontrollers are used in embedded applications. The safety-critical nature and prevalence of these applications demand that their correctness and safety should be rigorously verified.

This thesis presents techniques to apply deductive software verification to the embedded domain and implements them in the VESUV plugin for the VerCors verifier. In two parts, it discusses advances on two problems for embedded systems verification.

The first part of this thesis discusses an invariant generation technique for verifying global properties common to embedded systems, such as timing and process interaction, locally using deductive reasoning. The invariant generation uses abstract interpretation with automatic abstraction refinement to focus in on the relevant aspects of the system under verification and abstract from unnecessary details.

The second part of this thesis describes an approach for encoding embedded software, including aspects of its execution environment, to be analyzed with a deductive verifier. It presents an approach for reasoning about concepts relevant to embedded systems, such as timing, event reactivity, and hardware interaction. It explores these concepts on the examples of two common execution environments for embedded systems, the hardware/software co-design language SystemC and the popular real-time operating system FreeRTOS, and implements encodings of both in VESUV.