xTune: A Formal Methodology for Cross-layer Tuning of Mobile Real-time Embedded Systems

xTune: A Formal Methodology for Cross-layer Tuning of  Mobile Real-time Embedded Systems
by Minyoung Kim (Advisor: Prof. Nikil Dutt)
Date: July 8, 2008

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. One objective of this approach is to enable tradeoff analysis across multiple layers (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 desired 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 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 by treating a multimedia case study on resource-limited devices.