The public defense of Andreas Johnsen’s doctoral thesis in Computer Science and Engineering

Doctoral thesis and Licentiate seminars

Datum: 2018-01-26
Tid: 13.00
Plats: Room Gamma, MDH Västerås.

The public defense of Andreas Johnsen’s doctoral thesis in Computer Science and Engineering will take place at Mälardalen University (Västerås Campus) room Gamma, at 13.00 on January 26, 2018.

Title: “Quality Assurance for Dependable Embedded Systems”.

Serial number: 252

The faculty examiner is Professor Paola Inverardi, University of L’Aquila; and the examining committee consists of Professor Simin Nadjm-Tehrani, Linköping University; Professor Stefan Wagner, University of Stuttgart; Docent Patrizio Pelliccione, Chalmers University of Technology/University of Gothenburg.

Reserve; docent Moris Behnam, MDH.


The main goal of this doctoral thesis is to improve verification processes of dependable embedded systems. An embedded system is a computer system that has a dedicated function within a larger electrical and possibly mechanical system. A dependable embedded system is a computer system which function additionally is critical to the system it is embedded within. Examples of dependable embedded systems are electronic control systems in airplanes, trains, and cars, such as an autopilot. Since an incorrect operation of these systems may endanger people and the environment, it is crucial to verify that the systems achieve high quality before they are put into service. In this regard, verification means efforts that intend to detect and correct defects in the systems that are being developed.

Verification of embedded systems commonly involves manual work, which is becoming increasingly labor intensive and error prone due to the increasing complexity of the systems. The contribution of this doctoral thesis is a framework of verification techniques that provides an automated verification process, to reduce the cost of human labor and the risk of human error. A comprehensive set of verification techniques is included such that defects may be detected throughout the development process, including early design faults, intermediate implementation faults, and later maintenance faults. In addition, the framework is based on a mathematical foundation to ensure reliable verification results. Altogether, the framework provides a significant protection against costly and risky defects that may arise in the development of dependable embedded systems.

The performance and scalability of the verification framework are evaluated in this thesis by means of case studies, where, for example, it is applied to a safety-critical train control system. The results of the studies demonstrate a high fault detection rate and a scalability to advanced embedded systems with multi-core processors and multitasking.