danka_PhD

Verification of Component-based Embedded System Designs

Daniel Karlsson Author homepage

Ph. D. Thesis No. 1017, Dept. of Computer and Information Science, Linköping University, June 2006 (Opponent: Prof. Bashir Al-Hashimi, University of Southampton, UK)

Prof. Bashir Al-Hashimi, University of Southampton, UK

ABSTRACT


Embedded systems are becoming increasingly com­mon in our everyday lives. As technology progresses, these systems become more and more complex. Design­ers handle this increasing complexity by reusing existing compo­nents. At the same time, the systems must fulfill strict functional and non-functional requirements.

This thesis presents novel and efficient techniques for the ver­ification of component-based embedded system designs. As a common basis, these techniques have been developed using a Petri net based modelling approach, called PRES+.

Two complementary problems are addressed: component veri­fication and integration verification. With component verifica­tion the providers verify their components so that they function correctly if given inputs conforming to the assumptions imposed by the components on their environment.

Two techniques for component verification are proposed in the thesis. The first technique enables formal verification of Sys­temC designs by translating them into the PRES+ representa­tion. The second technique involves a simulation based approach into which formal methods are injected to boost verifi­cation efficiency.

Provided that each individual component is verified and is guaranteed to function correctly, the components are intercon­nected to form a complete system. What remains to be verified is the interface logic, also called glue logic, aronments as well as the underlying the­oretical framework and a step-by-step roadmap on how to apply these algorithms.

Experimental results have proven the efficiency of the pro­posed techniques and demonstrated that it is feasible to apply them on real-life examples.


Related files:
danka_PhD.pdfAdobe Acrobat portable document


[K06] Daniel Karlsson, "Verification of Component-based Embedded System Designs", Ph. D. Thesis No. 1017, Dept. of Computer and Information Science, Linköping University, June 2006 (Opponent: Prof. Bashir Al-Hashimi, University of Southampton, UK)
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)
Last modified on Monday December 04, 2006 by Gert Jervan