Luis Alejandro Cortes - Ph D abstract

Embedded computer systems have become ubiquitous. They are used in a wide
spectrum of applications, ranging from household appliances and mobile devices
to vehicle controllers and medical equipment.

This dissertation deals with design and verification of embedded systems, with a
special emphasis on the real-time facet of such systems, where the time at which
the results of the computations are produced is as important as the logical
values of these results. Within the class of real-time systems two categories,
namely hard real-time systems and soft real-time systems, are distinguished and
studied in this thesis.

First, we propose modeling and verification techniques targeted towards hard
real-time systems, where correctness, both logical and temporal, is of prime
importance. A model of computation based on Petri nets is defined. The model can
capture explicit timing information, allows tokens to carry data, and supports
the concept of hierarchy. Also, an approach to the formal verification of
systems represented in our modeling formalism is introduced, in which model
checking is used to prove whether the system model satisfies its required
properties expressed as temporal logic formulas. Several strategies for
improving verification efficiency are presented and evaluated.

Second, we present scheduling approaches for mixed hard/soft real-time systems.
We study systems that have both hard and soft real-time tasks and for which the
quality of results (in the form of utilities) depends on the completion time of
soft tasks. Also, we study systems for which the quality of results (in the form
of rewards) depends on the amount of computation allotted to tasks. We introduce
quasi-static techniques, which are able to exploit at low cost the dynamic slack
caused by variations in actual execution times, for maximizing utilities/rewards
and for minimizing energy.

Numerous experiments, based on synthetic benchmarks and realistic case studies,
have been conducted in order to evaluate the proposed approaches. The
experimental results show the merits and worthiness of the techniques introduced
in this thesis and demonstrate that they are applicable on real-life examples.



Travel reports

Licentiate seminars


Courses Spring 2015


Last modified on February 2005 by Anne Moe