[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 A Formal Methodology for Compositional Cross-Layer Optimization
Kim, Minyoung and Stehr, Mark-Oliver and Talcott, Carolyn and Dutt, Nikil and Venkatasubramanian, Nalini - 2011 - PDF

The xTune framework employs iterative tuning using light- weight formal verification at runtime with feedback for dynamic adapta- tion of mobile real-time embedded systems. To enable trade-off analysis across multiple layers of abstraction and predict the possible property violations as the system evolves dynamically over time, an executable formal specification is developed for each layer of the system under con- sideration. The formal specification is then analyzed using statistical analysis, to determine the impact of various policies for achieving a vari- ety 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 as- sociated layers. We also introduce sample application domains for future research directions.