Formal design of performance-driven self-adapting systems under uncertainty

Performance evaluation is fundamental for modern software systems design since it heavily determines users satisfaction. However, although standard quantitative methods are effective for studying the performance behavior of software in the early stage, they may fail at runtime when systems are exposed to strong external and internal variability (e.g., workload fluctuations or hardware degradation). In this setting, performance-driven self-adaptation is a promising technique. It manages runtime variability by continuously monitoring the current execution conditions and, when required, by triggering reconfiguration actions using a model of the system under study. This introduces three main difficulties: i) the system model must be efficiently analyzed, ii) an effective strategy for exploring the adaptation space (i.e., the set of all feasible system configurations) must be devised, iii) frequent up-to-date estimates of model parameters need to be provided in a minimally intrusive manner. Motivated by these challenges, this thesis studies the definition of performance-driven selfadaptation techniques enabling effective and efficient runtime reconfigurations. We focus on systems whose performance dynamics can be described by a compact, approximate representation of queuing networks based on ordinary differential equations. We exploit this representation of the system as the enabling technology for defining different performance-driven self-adaptation techniques following two orthogonal approaches. The symbolic approach is based on closed-form formulas expressing the steady-state relation between the system parameters and its throughput. The main contribution is an encoding of the performance-driven adaptation problem as a satisfiability modulo theories one. This allows querying for a feasible assignment of the system parameters that satisfy given performance requirements or getting a formal proof of its unavailability (i.e., no such a configuration exists). The numeric approach, instead, is founded on the numerical analysis of the dynamical model describing the transient performance behavior of the system. In this case, we formulate the performance-driven self-adaptation problem using model predictive control, a well-known technique based on online optimization. The main novel contribution in this area is the exact formulation of the original nonlinear runtime adaptation problem as a linear one, enabling faster adaptation space explorations. Finally, we propose a moving horizon estimator for the resource demands of queuing networks. Its main novelty lays in the formulation of the estimation problem as an efficient quadratic optimization one built on the observation of transient queue-length dynamics. This yields an accurate and nonintrusive estimation methodology employable as the input phase of any of the performance-driven adaptation techniques presented in this thesis.