luis-abstract
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.
|
