xTune: A Formal Methodology for Cross-layer Tuning
of Mobile Real-time Embedded Systems
[Home] [People] [News] [Publications] [Sponsors] [Links]
Resource
limited mobile real-time embedded systems can benefit greatly from dynamic
adaptation of
system parameters. This thesis proposes a novel framework,
xTune, that
employs iterative tuning using light-weight formal verification at runtime
with feedback
for dynamic adaptation of mobile real-time embedded systems.
One
objective of this approach is to enable tradeoff analysis across multiple
layers of
abstraction (for
example, application, middleware, operating system) and predict the
possible property
violations as the system evolves dynamically over time. Specifically,
an executable
formal specification is developed for each layer of the mobile real-time
system under
consideration. The formal specification is then analyzed using statistical
model checking
and statistical quantitative analysis, to determine the impact of
various resource
management policies for achieving a variety of end-to-end properties
in a
quantifiable manner. The integration of formal analysis with dynamic behavior
from system
execution results in a feedback loop that enables model refinement and
further optimization
of policies and parameters. Finally, we propose a composition
method for
coordinated interaction of optimizers at different abstraction layers. The
core idea of
our approach is that each participating optimizer can restrict its own
parameters
and exchange
refined parameters with its associated layers. We demonstrate
the
applicability of the proposed methodology to the adaptive provisioning of
mobile
real-time embedded
systems through a multimedia case study on resource-limited
mobile devices.