Methodology

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

The above figure presents the xTune framework that employs iterative tuning using light-weight, on-the-fly formal verification

with feedback for dynamic adaptation. We take three major steps:

 

1. Modeling, specification and reasoning about cross-layer timing properties:

     We propose a novel approach based on concurrent rewriting logic to formally specify and reason about timing issues

     at all levels of system granularity and study their interrelationships.

     [FMOODS’07]

 

2. Design of policies for addressing QoS/performance based on the cross-layer tradeoffs analysis:

     Our work examines the impact of various resource management techniques on end-to-end timing properties

     and enables informed selection of resource management policies along with rules for instantiation of parameters that drive the policies.

     [DATE’08]

 

3. Reinforcement and proactive control:

    We enhance our light-weight formal modeling and analysis by integrating it with system realization to achieve adaptive reasoning

    and proactive control by providing more precise information on current execution and future state.

    [FORMATS’07]

   

Online Verifiable Cross-Layer Adaptation for Distributed Real-Time Embedded Systems

xTune