Assurances for Self-Adaptive Systems

We propose to see adaptive systems as systems with highly dynamic features. We model as features both the reconfigurations of the system, but also the changes of the environment, such as failure modes. The resilience of the system can then be defined as the fact that the system can select an adequate reconfiguration for each possible change of the environment. We must take into account that reconfiguration is often a major undertaking for the system: it has a high cost and it might make functions of the system unavailable for some time. These constraints are domain-specific. In this paper, we therefore provide a modelling language to describe these aspects, and a property language to describe the requirements on the adaptive system. We design algorithms that determine how the system must reconfigure itself to satisfy its intended requirements.

An effective design of effective and efficient self-adaptive systems may rely on several existing approaches. Software models and model checking techniques at run time represent one of them since they support automatic reasoning about such changes, detect harmful configurations, and potentially enable appropriate (self-)reactions. However, traditional model checking techniques and tools may not be applied as they are at run time, since they hardly meet the constraints imposed by on-the-fly analysis, in terms of execution time and memory occupation. For this reason, efficient run-time model checking represents a crucial research challenge.

This paper precisely addresses this issue and focuses on probabilistic run-time model checking in which reliability models are given in terms of Discrete Time Markov Chains which are verified at run-time against a set of requirements expressed as logical formulae. In particular, the paper discusses the use of probabilistic model checking at run-time for self-adaptive systems by surveying and comparing the existing approaches divided in two categories: state-elimination algorithms and algebra-based algorithms. The discussion is supported by a realistic example and by empirical experiments.

Distributed applications in the cloud are composed of a set of virtual machines running a set of interconnected software components. In this context, setting up, (re)configuring, and monitoring these applications is a real burden since a software application may depend on several remote software and virtual machine configurations. These management tasks involve many complex protocols, which fully automate these tasks while preserving application consistency. In this paper, we focus on a self-configuration protocol, which is able to configure a whole distributed application without requiring any centralized server. The high degree of parallelism involved in this protocol makes its design complicated and error-prone. In order to check that this protocol works as expected, we specify it in LOTOS NT and verify it using the CADP toolbox. The use of these formal techniques and tools helped to detect a bug in the protocol, and served as a workbench to experiment with several possible communication models.

Self-* systems have the ability to adapt to a changing environment and to compensate component failures by reorganizing themselves. However, as these systems make autonomous decisions, their behavior is hard to predict. Without behavioral guarantees their acceptance, especially in safety critical applications, is arguable. This chapter presents a rigorous specification and verification approach for self-* systems that allows giving behavioral guarantees despite of the unpredictability of self-* properties. It is based on the Restore Invariant Approach that allows the developer to define a corridor of correct behavior in which the system shows the expected properties.

The approach defines relies (behavior the components can expect) and guarantees (behavior that each component will provide) to specify the general requirements on the interaction between the components of the system on a formal basis. If heterogeneous multi-agent systems with self-* properties are modeled so that relies are implied by the other components’ guarantees, it is possible to formally verify correct system behavior. When using observer/controller architectures the approach also allows systematic decomposition and modular verification. We illustrate the approach by applying it to two different case studies – an adaptive production cell and autonomous virtual power plants.

Self-healing can be used to reduce hazards in embedded real-time systems which are applied in safety-critical environments. These systems may react to failures by a structural reconfiguration of the architecture during runtime. This means the exchange of components or the modification of the components’ connections, in order to avoid that a failure results in a hazard. This reaction is subject to hard real-time constraints because reacting too late does not yield the intended effects. Consequently, it is necessary to analyze the propagation of failures in the architectural configuration over time with respect to the structural reconfiguration. However, current approaches do not take into account the timing properties of the failure propagation and the structural reconfiguration. In this paper, we present a hazard analysis approach which specifically considers these timing properties. We illustrate our approach by an example case study from the RailCab project. Further, we demonstrate the scalability of the approach by experiments.

Software is expected to become the dominant driver for innovation for the next generation of advanced distributed embedded real-time systems (advanced mechatronic systems). Software will build communities of autonomous agents at runtime which exploit local and global networking to enhance and optimize their functionality leading to self-adaptation or self-optimization. However, current development techniques are not capable of providing the safety guarantees required for this class of systems. Our approach, MechatronicUML, addresses the outlined challenge by proposing a coherent and integrated model-driven development approach which supports the modeling and verification of safety guarantees for systems with reconfiguration of software components at runtime. Modeling is based on a syntactically and semantically rigorously defined and partially refined subset of UML. Verification is based on a special type of decomposition and compositional model checking to make it scalable.

Internal faults but also external events, or misinterpretations of sensor inputs as well as failing actuator actions make developing dependable systems a demanding task. This holds especially in the case where systems heavily interact with their environment. Even in case that the most common faults can be handled, it is very unlikely to capture all possible faults or interaction patterns at development time. As a consequence self-adaptive systems that respond to certain unexpected actions and observations at runtime are required. A pre-requisite for such system behavior is that the system itself has knowledge about itself and its objectives, which can be used for adapting its behavior autonomously. In order to provide a methodology for such systems we propose the use of model-based reasoning as foundation for adaptive systems. Besides lying out the basic principles, which allow for assurance of correctness and completeness of the reasoning results with respect to the underlying system model, we show how these techniques can be used to build self-adaptive mobile robots. In particular the proposed methodology relies on model-based diagnosis in combination with planning. We also discuss modeling issues and show how modeling paradigms influences the outcome of model-based reasoning. Moreover, we introduce some case studies of self-adaptive systems that rely on model-based reasoning concepts in order to show their applicability in practice. The case studies include mobile robots that react on hardware and software failures by applying corrective actions like restarting subsystems or reconfiguration of system parameters.

Distributed pervasive systems have been employed in a wide spectrum of applications, from environmental monitoring to smart transportation, to emergency response. In all these applications high volumes of typically volatile software components need to coordinate and collaborate to achieve a common goal, given a defined set of constraints.

In our A-3 initiative we advocate that the coordination of high volumes of volatile components can be simplified using appropriate group abstractions. Instead of attempting to coordinate large amounts of components, the problem can be reduced to coordinating “groups” of components which have a less dynamic behavior. This abstraction effectively simplifies the design of self-adaptive behavior by making it easier to achieve component coordination. By design it also prevents the system from being flooded with coordination messages.

In this chapter we present an extension of our A-3 middleware called A3-TAG. It is a unified programming model that facilitates the system design. Moreover, the middleware internally adopts the same group abstractions to ensure that message exchanges, and in particular group broadcasts, are achieved efficiently and robustly. The chapter also presents an investigation of our approach in the context of a self-adaptive industrialized greenhouse.

As service-oriented systems are increasingly composed of third-party services accessible over the Internet, self-adaptation capabilities promise to make these systems become robust and resilient against third-party service failures that may negatively impact on system quality. In such a setting, proactive adaptation capabilities will provide significant benefits by predicting pending service failures and mitigating their negative impact on system quality. Proactive adaptation requires accurate quality prediction techniques; firstly, because executing unnecessary proactive adaptations (due to false positive predictions) might lead to additional costs or follow-up-failures; secondly, because proactive adaptation opportunities may be missed (due to false negative predictions). This book chapter reviews solutions for measuring and ensuring the accuracy of online service quality predictions. It critically analyses their applicability in the setting of third-party services and supports this analysis with empirical data.

Despite the best efforts of software engineers, faults still escape into deployed software. Developers need time to prepare and distribute fixes, and in the interim, deployments must either avoid failures or endure their consequences. Self-adaptive systems–systems that adapt to changes internally, in requirements, and in a dynamic environment– can often handle these challenges automatically, depending on the nature of the failures.

Those self-adaptive systems where functional features can be added or removed also constitute configurable systems. Configurable software is known to suffer from failures that appear only under certain feature combinations, and these failures are particularly challenging for testers, who must find suitable configurations as well as inputs to detect them. However, these elusive failures seem well suited for avoidance by self-adaptation. We need only find an alternative configuration that precludes the failure without derailing the current use case.

This work investigates that possibility, along with some further conjectures: that the failures that are sensitive to a system’s configuration depend on similar feature combinations–a phenomenon we call featurelocality– that this locality can be combined with historical data to predict failure-prone configurations and reconfiguration workarounds, and that these workarounds rarely lead the system out of one failure and into another. In a case study on 128 failures reported against released versions of an open source configurable system, and 16 failures discovered through a state-of-the-art testing tool, plus several thousand tests cases, we find evidence to support all of these hypotheses.

The demand for cost effectiveness and increased flexibility has driven the fast-paced adoption of software systems in areas where requirement violations may lead to financial loss or loss of life. Many of these software systems need to deliver not only high integrity but also self adaptation to the continual changes that characterise such application areas. A challenge long solved by control theory for continuous-behaviour systems was thus reopened in the realm of software systems. Software engineering needs to embark on a quest for self-adaptive high-integrity software. This paper explains the growing need for software capable of both self-adaptation and high integrity, and explores the starting point for the quest to make it a reality. We overview emerging techniques for the engineering of self-adaptive high-integrity software, propose a service-based architecture that aims to integrate these techniques, and discuss opportunities for future research.

In this paper we discuss the assurance of self-adaptive controllers for the Cloud, and we propose a taxonomy of controllers based on the supported assurance level. Self-adaptive systems for the Cloud are commonly built by means of controllers that aim to guarantee the required quality of service while containing costs, through a careful allocation of resources. Controllers determine the allocation of resources at runtime, based on the inputs and the status of the system, and referring to some knowledge, usually represented as adaptation rules or models. Assuring the reliability of self-adaptive controllers account to assuring that the adaptation rules or models represent well the system evolution. In this paper, we identify different categories of control models based on the assurance approaches. We introduce two main dimensions that characterize control models. The dimensions refer to the flexibility and scope of the system adaptability, and to the accuracy of the assurance results. We group control models in three main classes that depend on the kind of supported assurance that may be checked either at design or runtime. Controllers that support assurance of the control models at design time privilege reliability over adaptability. They usually represent the system at a high granularity level and come with high costs. Controllers that support assurance of the control models at runtime privilege adaptability over reliability. They represent the system at a finer granularity level and come with reduced costs. Controllers that combine different models may balance verification at design and runtime and find a good trade off between reliability, adaptability, granularity and costs.