Towards Formal Planning for Quality-aware Self-Adaptive Systems

Self-adaptive systems (SAS) have the ability to achieve functional and/or quality of service objectives by automatically modifying their behavior at runtime. Accordingly, each self-adaptive system typically consists of a managed system dealing with the domain concerns, and a feedback loop handling adaptation concerns of the managed system. In the aim to promote the actual use of these systems, it is necessary to cope with underlying uncertainty and variability of their execution environments. However, existing approaches lack formal models and/or tools to engineer all aspects of self-adaptation. In this paper, we propose a formal approach for modeling, developing and analyzing quality-aware SASs under uncertainty. We mainly focus on non-deterministic selection of adaptation plans. The approach is based on probabilistic rewrite theories to address adaptation planning. The formal model is defined using PSMAUDE which allows specifying nonfunctional requirements, strategies and probabilistic systems features.