[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 xTune: A Formal Methodology for Cross-layer Tuning of Mobile Embedded Systems
Kim, Minyoung and Stehr, Mark-Oliver and Talcott, Carolyn and Dutt, Nikil and Venkatasubramanian, Nalini - 2011 - PDF

Resource-limited mobile embedded systems can benefit greatly from dynamic adaptation of sys- tem parameters. We propose a novel approach that employs iterative tuning using light-weight formal verification at runtime with feedback for dynamic adaptation. One objective of this ap- proach is to enable tradeoff analysis across multiple layers (e.g., application, middleware, OS) and predict the possible property violations as the system evolves dynamically over time. Specif- ically, an executable formal specification is developed for each layer of the mobile system under consideration. The formal specification is then analyzed using statistical property checking and statistical quantitative analysis, to determine the impact of various resource management policies for achieving desired timing/QoS properties. Integration of formal analysis with dynamic behav- ior from system execution results in a feedback loop that enables model refinement and further optimization of policies and parameters. We demonstrate the applicability of this approach to the adaptive provisioning of resource-limited distributed real-time systems using a mobile multimedia case study.

Keywords: Cross-Layer Optimization, Iterative Tuning, Formal Methods