Solving the next adaptation problem with prometheus

Dealing with multiple requirement failures is an essential capability for self-adaptive software systems. This capability becomes more challenging in the presence of conflicting goals. This paper is concerned with the next adaptation problem: the problem of finding the best next adaptation in the presence of multiple failures. `Best' here means that the adaptation chosen optimizes a given set of objective functions, such as the cost of adaptation or the degree of failure for system requirements. The paper proposes a formal framework for defining the next adaptation problem, assuming that we can specify quantitatively the constraints that hold between indicators that measure the degree of failure of each requirement and control parameters. These constraints, along with one or several objective functions, are translated into a constrained multi-objective optimization problem that can be solved by using an OMT/SMT (Optimization Modulo Theories/Satisfiability Modulo Theories) solver, such as OptiMathSAT. The proposed framework is illustrated with the Meeting Scheduler exemplar and a second, e-shop case study.