Synthesizing Pareto optimal decision for autonomic clouds using stochastic games model checking

The ability to automatically generate and guarantee the optimal decision for self-adaptation is important especially when there are multiple quality objectives that need to be satisfied, the uncertainties in the adaptation outcome, and the time-varying resource demands, especially in the autonomic cloud systems. To address this issue, in this paper, we propose an approach to automatically encode the adaptation decision behavior and the multiple quality objectives, as well as synthesizing the behaviour to fulfill the specified objectives. In the approach, we emphasize the relation between quality objectives expressed as a variant of temporal logic specification and the domain-specific Service Level Agreements (SLA) (i.e. cloud environment). The approach also covers the abstraction method for representing the adaptation behavior as stochastic games, and the re-synthesis method to adjust the threshold values, if failing to satisfy the predefined thresholds. We apply the stochastic games model checking with strategy synthesis to realize the approach. The Pareto-set computation is utilized to support the adjustment of threshold values. We present a set of validation results to show the effectiveness and performance of the proposed approach.