Abstract: Self-adaptive systems must decide which adaptations to apply and when. In reactive approaches, adaptations are chosen and executed after some issue in the system has been detected (e.g., unforeseen attacks or failures). In proactive approaches, predictions are used to prepare the system for some future event (e.g., traffic spikes during holidays). In both cases, the choice of adaptation is based on the estimated impact it will have on the system. Current decision-making approaches assume that the impact will be instantaneous, whereas it is common that adaptations take time to produce their impact. Ignoring this latency is problematic because adaptations may not achieve their effect in time for a predicted event. Furthermore, lower impact but quicker adaptations may be ignored altogether, even if over time the accrued impact is actually higher. In this article, we introduce a novel approach to choosing adaptations that considers these latencies. To show how this improves adaptation decisions, we use a two-pronged approach: (i) model checking of Stochastic Multiplayer Games (SMGs) enables us to understand best- and worst-case scenarios of optimal latency-aware and non-latency-aware adaptation without the need to develop specific adaptation algorithms. However, since SMGs do not provide an algorithm to make choices at runtime, we propose a (ii) latency-aware adaptation algorithm to make decisions at runtime. Simulations are used to explore more detailed adaptation behavior and to check if the performance of the algorithm falls within the bounds predicted by SMGs. Our results show that latency awareness improves adaptation outcomes and also allows a larger set of adaptations to be exploited.

Abstract: Design decisions made during early development stages of self-adaptive systems tend to have a significant impact upon system properties at runtime (e.g., safety, QoS). However, understanding the implications of these decisions a priori is difficult due to the different types and degrees of uncertainty that affect such systems (e.g., simplifying assumptions, human-in-the-loop). To provide some assurances about self-adaptive system designs, evidence can be gathered from activities such as simulations and prototyping, but these demand a significant effort and do not provide a systematic way of dealing with uncertainty. In this chapter, we describe an approach based on model checking of stochastic multiplayer games (SMGs) that enables developers to approximate the behavioral envelope of a self-adaptive system by analyzing best- and worst-case scenarios of alternative designs for self-adaptation mechanisms. Compared to other sources of evidence, such as simulations or prototypes, our approach provides developers with a preliminary understanding of adaptation behavior with less effort, and without the need to have any specific adaptation algorithms or infrastructure in place. We illustrate our approach by showing how it can be used to mitigate different types of uncertainty in contexts such as self-protecting systems, proactive latency-aware adaptation, and human-in-the-loop.

Abstract: Software systems are increasingly called upon to autonomously manage their goals in changing contexts and environments, and under evolving requirements. In some circumstances, autonomous systems cannot be fully automated but instead cooperate with human operators to maintain and adapt themselves. Furthermore, there are times when a choice should be made between doing a manual or automated repair. Involving operators in self-adaptation should itself be adaptive, and consider aspects such as the training, attention, and ability of operators. Not only do these aspects change from person to person, but they may change with the same person. These aspects make the choice of whether to involve humans non-obvious. Self-adaptive systems should trade-off whether to involve operators, taking these aspects into consideration along with other business qualities it is attempting to achieve. In this chapter, we identify the various roles that operators can perform in cooperating with self-adaptive systems. We focus on humans as effectors - doing tasks which are difficult or infeasible to automate. We describe how we modified our self-adaptive framework, Rainbow, to involve operators in this way, which involved choosing suitable human models and integrating them into the existing utility trade-off decision models of Rainbow. We use probabilistic modeling and quantitative verification to analyze the trade-offs of involving humans in adaptation, and complement our study with experiments to show how different business preferences and modalities of human involvement may result in different outcomes.

Abstract: Many self-adaptive systems benefit from human involvement, where a human operator can provide expertise not available to the system and perform adaptations involving physical changes that cannot be automated. However, a lack of transparency and intelligibility of system goals and the autonomous behaviors enacted to achieve them may hinder a human operator's effort to make such involvement effective. Explanation is sometimes helpful to allow the human to understand why the system is making certain decisions. However, explanations come with costs in terms of, e.g., delayed actions. Hence, it is not always obvious whether explanations will improve the satisfaction of system goals and, if so, when to provide them to the operator. In this work, we define a formal framework for reasoning about explanations of adaptive system behaviors and the conditions under which they are warranted. Specifically, we characterize explanations in terms of their impact on a human operator's ability to effectively engage in adaptive actions. We then present a decision-making approach for planning in self-adaptation that leverages a probabilistic reasoning tool to determine when the explanation should be used in an adaptation strategy in order to improve overall system utility. We illustrate our approach in a representative scenario for the application of an adaptive news website in the context of potential denial-of-service attacks.

Abstract: Knowledge-intensive processes (KiPs) are processes characterized by high levels of unpredictability and dynamism. Their process structure may not be known before their execution. One way to cope with this uncertainty is to defer decisions regarding the process structure until run time. In this paper, we consider the definition of the process structure as a planning problem. Our approach uses automated planning techniques to generate plans that define process models according to the current context. The generated plan model relies on a metamodel called METAKIP that represents the basic elements of KiPs. Our solution explores Markov Decision Processes (MDP) to generate plan models. This technique allows uncertainty representation by defining state transition probabilities, which gives us more flexibility than traditional approaches. We construct an MDP model and solve it with the help of the PRISM model-checker. The solution is evaluated by means of a proof of concept in the medical domain and reveals the feasibility of our approach.

Abstract: Modern software systems are often compositions of entities that increasingly use self-adaptive capabilities to improve their behavior to achieve systematic quality goals. Self-adaptive managers for each component system attempt to provide locally optimal results, but if they cooperated and potentially coordinated their efforts it might be possible to obtain more globally optimal results. The emergent properties that result from such composition and cooperation of self-adaptive systems are not well understood, difficult to reason about, and present a key challenge in the evolution of modern software systems. For example, the effects of coordination patterns and protocols on emergent properties such as the resiliency of the collectives need to be understood when designing these systems. In this paper we propose that probabilistic model checking of stochastic multiplayer games (SMG) provides a promising approach to analyze, understand, and reason about emergent properties in collectives of adaptive systems (CAS). Probabilistic Model Checking of SMGs is a technique particularly suited to analyzing emergent properties in CAS, since SMG models capture: (i) the uncertainty and variability intrinsic to the CAS and its execution environment in the form of probabilistic and nondeterministic choices, and (ii) the competitive/cooperative aspects of the interplay among the constituent systems of the CAS. Analysis of SMGs allows us to reason about things like the worst case scenarios, which constitutes a new contribution to understanding emergent properties in CAS. We investigate the use of SMGs to show how they can be useful in analyzing the impact of communication topology for collections of fully cooperative systems defending against an external attack.

Abstract: Self-adaptive systems tend to be reactive and myopic, adapting in response to changes without anticipating what the subsequent adaptation needs will be. Adapting reactively can result in ineffi?ciencies due to the system performing a suboptimal sequence of adaptations. Furthermore, when adaptations have latency, and take some time to produce their e?ffect, they have to be started with su?fficient lead time so that they complete by the time their eff?ect is needed. Proactive latency-aware adaptation addresses these issues by making adaptation decisions with a look-ahead horizon and taking adaptation latency into account. In this paper we present an approach for proactive latency-aware adaptation under uncertainty that uses probabilistic model checking for adaptation decisions. The key idea is to use a formal model of the adaptive system in which the adaptation decision is left underspeci?fied through nondeterminism, and have the model checker resolve the nondeterministic choices so that the accumulated utility over the horizon is maximized. The adaptation decision is optimal over the horizon, and takes into account the inherent uncertainty of the environment predictions needed for looking ahead. Our results show that the decision based on a look-ahead horizon, and the factoring of both tactic latency and environment uncertainty, considerably improve the eff?ectiveness of adaptation decisions.

Abstract: Self-adaptive systems overcome many of the limitations of human supervision in complex software-intensive systems

by endowing them with the ability to automatically adapt their

structure and behavior in the presence of runtime changes.

However, adaptation in some classes of systems (e.g., safety- critical) can benefit by receiving information from humans (e.g.,

acting as sophisticated sensors, decision-makers), or by involving

them as system-level effectors to execute adaptations (e.g., when

automation is not possible, or as a fallback mechanism). However,

human participants are influenced by factors external to the

system (e.g., training level, fatigue) that affect the likelihood

of success when they perform a task, its duration, or even if

they are willing to perform it in the first place. Without careful

consideration of these factors, it is unclear how to decide when to

involve humans in adaptation, and in which way. In this paper,

we investigate how the explicit modeling of human participants

can provide a better insight into the trade-offs of involving

humans in adaptation. We contribute a formal framework to

reason about human involvement in self-adaptation, focusing on

the role of human participants as actors (i.e., effectors) during

the execution stage of adaptation. The approach consists of:

(i) a language to express adaptation models that capture factors

affecting human behavior and its interactions with the system,

and (ii) a formalization of these adaptation models as stochastic

multiplayer games (SMGs) that can be used to analyze human- system-environment interactions. We illustrate our approach in

an adaptive industrial middleware used to monitor and manage

sensor networks in renewable energy production plants.

Abstract: Architecture-based approaches to self-adaptation rely on architectural descriptions to reason about the best way of adapting the structure and behavior of software-intensive systems at run time, either by choosing among a set of predefined adaptation strategies, or by automatically generating adaptation plans. Predefined strategy selection has allow computational overhead and facilitates dealing with uncertainty (e.g., by accounting explicitly for contingencies derived from unexpected outcomes of actions), but requires additional designer effort regarding the specification of strategies and is unable to guarantee optimal solutions. In contrast, run time plan generation is able to explore a richer solution space and provide optimal solutions in some cases, but is more limited when dealing with uncertainty, and incurs higher computational overheads. In this paper, we propose an approach to optimal adaptation plan generation for architecture-based self-adaptation via model checking of stochastic multiplayer games (SMGs). Our approach enables: (i) trade-off analysis among different qualities by means of utility functions and preferences, and (ii) explicit modeling of uncertainty in the outcome of adaptation actions and the behavior of the environment. Basing on the concepts embodied in the Rainbow framework for self-adaptation, we illustrate our approach in Znn.com, a case study that reproduces the infrastructure for a news website.