Luis Alejandro Cortes - Ph D abstract
Embedded computer systems have become ubiquitous. They are used in a
spectrum of applications, ranging from household appliances and mobile
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
the results of the computations are produced is as important as the
values of these results. Within the class of real-time systems two
namely hard real-time systems and soft real-time systems, are
studied in this thesis.
First, we propose modeling and verification techniques targeted towards
real-time systems, where correctness, both logical and temporal, is of
importance. A model of computation based on Petri nets is defined. The
capture explicit timing information, allows tokens to carry data, and
the concept of hierarchy. Also, an approach to the formal verification
systems represented in our modeling formalism is introduced, in which
checking is used to prove whether the system model satisfies its
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
We study systems that have both hard and soft real-time tasks and for
quality of results (in the form of utilities) depends on the completion
soft tasks. Also, we study systems for which the quality of results (in
of rewards) depends on the amount of computation allotted to tasks. We
quasi-static techniques, which are able to exploit at low cost the
caused by variations in actual execution times, for maximizing
and for minimizing energy.
Numerous experiments, based on synthetic benchmarks and realistic case
have been conducted in order to evaluate the proposed approaches. The
experimental results show the merits and worthiness of the techniques
in this thesis and demonstrate that they are applicable on real-life