ola-abstract.shtml
Ph D abstract - Daniel Karlsson
Verification of Component-based Embedded System Designs
Embedded systems are becoming increasingly common in our everyday
lives. As technology progresses, these systems become more and more
complex. Designers handle this increasing complexity by reusing
existing components. At the same time, the systems must fulfill strict
functional and non-functional requirements.
This thesis presents novel and efficient techniques for the
verification 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 verification and
integration verification. With component verification 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 SystemC designs by
translating them into the PRES+ representation. The second technique
involves a simulation based approach into which formal methods are
injected to boost verification efficiency.
Provided that each individual component is verified and is guaranteed
to function correctly, the components are interconnected to form a
complete system. What remains to be verified is the interface logic,
also called glue logic, and the interaction between components.
Each glue logic and interface cannot be verified in isolation. It must
be put into the context in which it is supposed to work. An appropriate
environment must thus be derived from the components to which the glue
logic is connected. This environment must capture the essential
properties of the whole system with respect to the properties being
verified. In this way, both the glue logic and the interaction of
components through the glue logic are verified. The thesis presents
algorithms for automatically creating such environments as well as the
underlying theoretical framework and a step-by-step roadmap on how to
apply these algorithms.
Experimental results have proven the efficiency of the proposed
techniques and demonstrated that it is feasible to apply them on
real-life examples.
|
