Abstract: Designing software in a way that guarantees run-time behavior while achieving an acceptable balance among multiple quality attributes is an open problem. Providing guarantees about the satisfaction of the same requirements under uncertain environments is even more challenging. Tools and techniques to inform engineers about poorly-understood design spaces in the presence of uncertainty are needed, so that engineers can explore the design space, especially when tradeoffs are crucial. To tackle this problem, we describe an approach that combines synthesis of spaces of system design alternatives from formal specifications of architectural styles with probabilistic formal verification. The main contribution of this paper is a formal framework for specification-driven synthesis and analysis of design spaces that provides formal guarantees about the correctness of system behaviors and satisfies quantitative properties (e.g., defined over system qualities) subject to uncertainty, which is treated as a first-class entity. We illustrate our approach in two case studies: a service-based adaptive system and a mobile robotics architecture. Our results show how the framework can provide useful insights into how average case probabilistic guarantees can differ from worst case guarantees, emphasizing the relevance of combining quantitative formal verification methods with structural synthesis, in contrast with techniques based on simulation and dynamic analysis that can only provide estimates about average case probabilistic properties.

Abstract: An increasingly important requirement for certain classes of software-intensive systems is the ability to self-adapt their structure and behavior at run-time when reacting to changes that may occur to the system, its environment, or its goals. A major challenge related to self-adaptive software systems is the ability to provide assurances of their resilience when facing changes. Since in these systems, the components that act as controllers of a target system incorporate highly complex software, there is the need to analyze the impact that controller failures might have on the services delivered by the system. In this paper, we present a novel approach for evaluating the resilience of self-adaptive software systems by applying robustness testing techniques to the controller to uncover failures that can affect system resilience. The approach for evaluating resilience, which is based on probabilistic model checking, quantifies the probability of satisfaction of system properties when the target system is subject to controller failures. The feasibility of the proposed approach is evaluated in the context of an industrial middleware system used to monitor and manage highly populated networks of devices, which was implemented using the Rainbow framework for architecture-based self-adaptation.

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: Self-adaptive software systems adapt to changes in the environment, in the system itself, in their requirements, or in their business objectives. Typically, these systems attempt to maintain system goals at run time and often provide assurance that they will meet their goals under dynamic and uncertain circumstances. While significant research has focused on ways to engineer selfadaptive capabilities into both new and legacy software systems, less work has been conducted on how to assure that self-adaptation maintains system goals. For traditional, especially safety-critical software systems, assurance techniques decompose assurances into sub-goals and evidence that can be provided by parts of the system. Existing approaches also exist for composing assurances, in terms of composing multiple goals and composing assurances in systems of systems. While some of these techniques may be applied to self-adaptive systems, we argue that several significant challenges remain in applying them to self-adaptive systems in this chapter. We discuss how existing assurance techniques can be applied to composing and decomposing assurances for self-adaptive systems, highlight the challenges in applying them, summarize existing research to address some of these challenges, and identify gaps and opportunities to be addressed by future research.

Abstract: Providing assurances for self-adaptive systems is challenging. A primary underlying problem is uncertainty that may stem from a variety of different sources, ranging from incomplete knowledge to sensor noise and uncertain behavior of humans in the loop. Providing assurances that the self-adaptive system complies with its requirements calls for an enduring process spanning the whole lifetime of the system. In this process, humans and the system jointly derive and integrate new evidence and arguments, which we coined perpetual assurances for self-adaptive systems. In this paper, we provide a background framework and the foundation for perpetual assurances for self-adaptive systems. We elaborate on the concrete challenges of offering perpetual assurances, requirements for solutions, realization techniques and mechanisms to make solutions suitable. We also present benchmark criteria to compare solutions. We then present a concrete exemplar that researchers can use to assess and compare approaches for perpetual assurances for self-adaptation

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 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.