Abstract: This paper focuses on the problem of optimizing system utility of Machine-Learning (ML) based systems in the presence of ML mispredictions. This is achieved via the use of self-adaptive systems and through the execution of adaptation tactics, such as model retraining, which operate at the level of individual ML components. To address this problem, we propose a probabilistic modeling framework that reasons about the cost/benefit trade-offs associated with adapting ML components. The key idea of the proposed approach is to decouple the problems of estimating (i) the expected performance improvement after adaptation and (ii) the impact of ML adaptation on overall system utility. We apply the proposed framework to engineer a self-adaptive ML-based fraud-detection system, which we evaluate using a publicly-available, real fraud detection data-set. We initially consider a scenario in which information on model’s quality is immediately available. Next we relax this assumption by integrating (and extending) state-of-the-art techniques for estimating model’s quality in the proposed framework. We show that by predicting the system utility stemming from retraining a ML component, the probabilistic model checker can generate adaptation strategies that are significantly closer to the optimal, as compared against baselines such as periodic or reactive retraining.

Abstract: As software systems become more complex the overall system structure -- or software architecture -- becomes a central design problem. An important step towards an engineering discipline of software is a formal basis for describing and analyzing these designs. In this paper we present a formal approach to one aspect of architectural design: the interactions between components. The key idea is to define architectural connectors as explicit semantic entities. These are specified as a collection of protocols that characterize each of the participant roles in an interaction and how these roles interact. We illustrate how this scheme can be used to define a variety of common architectural connectors. We further provide a formal semantics and show how this leads to a system in which architectural compatibility can be checked in a way analogous to type checking in programming languages.

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: Machine Learning (ML) is increasingly used in domains such as cyber-physical systems and enterprise systems. These systems typically operate in non-static environments, prone to unpredictable changes that can adversely impact the accuracy of the ML models, which are usually in the critical path of the systems. Mispredictions of ML components can thus affect other components in the system, and ultimately impact overall system utility in non-trivial ways. From this perspective, self-adaptation techniques appear as a natural solution to reason about how to react to environment changes via adaptation tactics that can potentially improve the quality of ML models (e.g., model retrain), and ultimately maximize system utility. However, adapting ML components is non-trivial, since adaptation tactics have costs and it may not be clear in a given context whether the benefits of ML adaptation outweigh its costs. In this paper, we present a formal probabilistic framework, based on model checking, that incorporates the essential governing factors for reasoning at an architectural level about adapting ML classifiers in a system context. The proposed framework can be used in a self-adaptive system to create adaptation strategies that maximize rewards of a multidimensional utility space. Resorting to a running example from the enterprise systems domain, we show how the proposed framework can be employed to determine the gains achievable via ML adaptation and to find the boundary that renders adaptation worthwhile.

Abstract: Software systems are designed and implemented with assumptions about the environment. However, once the system is deployed,the actual environment may deviate from its expected behavior,possibly undermining desired properties of the system. To enable systematic design of systems that are robust against potential environmental deviations, we propose a rigorous notion of robustness for software systems. In particular, the robustness of a system is de-fined as the largest set of deviating environmental behaviors under which the system is capable of guaranteeing a desired property. We describe a new set of design analysis problems based on our notion of robustness, and a technique for automatically computing robustness of a system given its behavior description. We demonstrate potential applications of our robustness notion on two case studies involving network protocols and safety-critical interfaces.

Abstract: Many self-adaptive systems benefit from human involvement and oversight, where a human operator can provide expertise not available to the system and can detect problems that the system is unaware of. One way of achieving this is by placing the human operator on the loop – i.e., providing supervisory oversight and intervening in the case of questionable adaptation decisions. To make such interaction effective, explanation is sometimes helpful to allow the human to understand why the system is making certain decisions and calibrate confidence from the human perspective. However, explanations come with costs in terms of delayed actions and the possibility that a human may make a bad judgement. Hence, it is not always obvious whether explanations will improve overall utility and, if so, what kinds of explanation to provide 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 explanation content, effect, and cost. We then present a dynamic adaptation approach that leverages a probabilistic reasoning technique to determine when the explanation should be used in order to improve overall system utility.

Abstract: Self-adaptive systems increasingly need to reason about and adapt both structural and behavioral system aspects, such as in mobile service robots, which must reason about missions that they need to achieve and the architecture of the software executing them. Deciding how to best adapt these systems to run time changes is challenging because it entails considering mutual dependencies between the software architecture that the system is running and the outcome of plans for completing tasks, while also considering multiple trade-offs and uncertainties. Considering all these aspects in planning for adaptation often yields large solution spaces which cannot be adequately explored at run time. We address this challenge by proposing a planning approach able to consider the impact of mutual dependencies between software architecture and task planning on the satisfaction of mission goals. The approach is able to reason quantitatively about the outcome of adaptation decisions handling both the reconfiguration of the system's architecture and adaptation of task plans under uncertainty and in a rich trade-off space. Our results show: (i) feasibility of run-time decision-making for self-adaptation in an otherwise intractable solution space by dividing-and-conquering adaptation into architecture reconfiguration and task planning sub-problems, and (ii) improved quality of adaptation decisions with respect to decision making that does not consider dependencies between architecture and task planning.

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: Microservice application developers try to mitigate the impact of partial outages typically by implementing service-to-service interactions that use well-known resiliency patterns, such as Retry, Fail Fast, and Circuit Breaker. However, those resiliency patterns–as well as their available open-source implementations–are often documented informally, leaving it up to application developers to figure out when and how to use those patterns in the context of a particular microservice application. In this paper, we take a first step towards improving on this situation by introducing a model checking-based approach in which we use the PRISM probabilistic model checker to analyze the behavior of the Retry and Circuit Breaker resiliency patterns as continuous-time Markov chains (CTMC). This approach has enabled us to quantify the impact of applying each resiliency pattern on multiple quality attributes, as well as to determine how to best tune their parameters to deal with varying service availability conditions, in the context of a simple client-service interaction scenario.

Abstract: Design and verification of modern systems requires diverse models, which often come from a variety of disciplines, and it is challenging to manage their heterogeneity – especially in the case of cyber-physical systems. To check consistency between models, recent approaches map these models to flexible static abstractions, such as architectural views. This model integration approach, however, comes at a cost of reduced expressiveness because complex behaviors of the models are abstracted away. As a result, it may be impossible to automatically verify important behavioral properties across multiple models, leaving systems vulnerable to subtle bugs. This paper introduces the Integration Property Language (IPL) that improves integration expressiveness using modular verification of properties that depend on detailed behavioral semantics while retaining the ability for static system-wide reasoning. We prove that the verification algorithm is sound and analyze its termination conditions. Furthermore, we perform a case study on a mobile robot to demonstrate IPL is practically useful and evaluate its performance.

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: Internet of Things (IoT) allows for cyber-physical applications to be created and composed to provide intelligent support or automation of end-user tasks. For many of such tasks, human participation is crucial to the success and the quality of the tasks. The cyber systems should proactively request help from the humans to accomplish the tasks when needed. However, the outcome of such system-human synergy may be affected by factors external to the systems. Failure to consider those factors when involving human participants in the tasks may result in suboptimal performance and negative experience on the humans. In this paper, we propose an approach for automated generation of control strategies of cyber-human systems. We investigate how explicit modeling of human participant can be used in automated planning to generate cooperative strategy of human and system to achieve a given task, by means of which best and appropriately utilize the human. Specifically, our approach consists of: (1) a formal framework for modeling cooperation between cyber system and human, and (2) a formalization of system-human cooperative task planning as strategy synthesis of stochastic multiplayer game. We illustrate our approach through an example of indoor air quality control in smart homes.

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

Abstract: While publish-subscribe systems have good engineering properties, they are difficult to reason about and to test. Model checking such systems is an attractive alternative. However, in practice coming up with an appropriate state model for a pub-sub system can be a difficult and error-prone task. In this paper we address this problem by describing a generic pub-sub model checking framework. The key feature of this framework is a reusable, parameterized state machine model that captures pub-sub runtime event management and dispatch policy. Generation of models for specific pub-sub systems is then handled by a translation tool that accepts as input a set of pub-sub component descriptions together with a set of pub-sub properties, and maps them into the framework where they can be checked using off-the-shelf model checking tools.

Abstract: While implicit invocation (publish-subscribe) systems have good engineering properties, they are difficult to reason about and to test. Model checking such systems is an attractive alternative. However, it is not clear what kinds of state models are best suited for this. In this paper we propose a structural approach, which factors the model checking problem into two parts: behavior specific to a particular implicit invocation system, and reusable runtime infrastructure that handles event-based communication and delivery policies. The reusable portion is itself structured so that alternative runtime mechanisms may be experimented with.

Abstract: Planning is one of the fundamental design considerations when building a selfadaptive software system. Planning helps the adaptive system to determine an appropriate course of action at run time that seeks to change the system's behavior in response to faults, changing environments and security threats. Therefore, having an appropriate planner to find a plan is critical to a successful self-adaptation.

For many adaptive systems, an appropriate planner is the one that not only finds a plan quickly, particularly, in urgent circumstances but also the plan provides a near-optimal long-term performance. However, due to the fundamental trade-off between quality and timeliness of planning, today designers often have to compromise between an approach that finds a plan quickly and an approach that is slow but finds a higher-quality plan.

To deal with this trade-off, this thesis proposes a hybrid planning approach for self-adaptive systems that combines of-the-shelf deliberative and reactive planners to find a balance between quality and timeliness. The key idea is to use reactive planning to provide a quick (although potentially a sub-optimal) response, but simultaneously invoke deliberative planning to determine quality plans. Once the deliberative plan is ready, it takes over the execution from the reactive plan to provide a higher quality adaptation thereafter.

Such a combination of planners can, in principle, reap the benefits of both worlds: providing plans quickly when the timing is critical, while allowing (nearly) optimal plans to be generated when the system has sufficient time to do so. Moreover, instead of going through the non-trivial process of developing a new algorithm/heuristic, hybrid planning combines off-the-shelf planners; therefore, hybrid planning does not require software engineers to master the complexity of developing new planning algorithms/heuristics.

This thesis demonstrates that, compared to its constituent reactive and deliberative planners, hybrid planning can find a better balance between the timeliness and the quality of planning, thereby improve adaptation effectiveness as measured by a multidimensional utility function capturing different dimensions of a system's goal. In the process, the thesis makes contributions to both the theory and the practice of hybrid planning in self-adaptive systems. Specifically, the thesis provides: (a) a formal framework defining the problem of hybrid planning; (b) a practical approach (grounded in the formal model) to apply hybrid planning to self-adaptive systems; (c) informal guidelines and a quantitative approach to help engineers to select an appropriate set of planners to instantiate hybrid planning for a given domain, and (d) evaluation of hybrid planning using two realistic systems to bridge the gap between theory and practice.