Abstract: Cyber-physical systems (CPS) are heterogeneous, because they tightly couple computation, communication and control along with physical dynamics, which are traditionally considered separately. Without a comprehensive modeling formalism, model-based development of CPS involves using a multitude of models in a variety of formalisms that capture various aspects of the system design, such as software design, networking design, physical models, and protocol design. Without a rigorous unifying framework, system integration and integration of the analysis results for various models remains ad hoc. In this paper, we propose a multi-view architecture framework that treats models as views of the underlying system structure and uses structural and semantic mappings to ensure consistency and enable system-level verification from that of the models in a hierarchical and compositional manner. Throughout the paper, the theoretical concepts are illustrated using two examples, an automotive intersection collision avoidance system and a quadrotor.

Abstract: As new market opportunities, technologies, platforms, and frameworks become available, systems require large-scale and systematic architectural restructuring to accommodate them. Today’s architects have few techniques to help them plan this architecture evolution. In particular, they have little assistance in planning alternative evolution paths, trading off various aspects of the different paths, or knowing best practices for particular domains. In this paper we describe an approach for planning and reasoning about architecture evolution. Our approach focuses on providing architects with the means to model prospective evolution paths and supporting analysis to select among these candidate paths. To demonstrate the usefulness of our approach, we show how it can be applied to an actual architecture evolution. In addition, we present some theoretical results about our evolution path constraint specification language.

Abstract: Software architecture allows us to make many decisions about a software system and analyze it even before it has been implemented, so as to make planned development possible. Similarly, architecture-based software evolution planning makes planned evolution possible by allowing us to make many decisions about the evolution of a software system and to analyze its evolution at the level of architecture design before software evolution is realized. In this paper, we develop a framework for architecture-based software evolution planning. It is done by defining various foundational terms and concepts, providing a taxonomy of software evolution plans, and then showing how to calculate values for various types of plans. By identifying and defining constituent foundational concepts, this conceptual framework makes precise the notion of ‘architecture-based software planning’. By developing a value-calculation framework for software evolution plans, it also provides a basis for concrete methods for designing and evaluating evolution plans.

Abstract: Development of modern Cyber-Physical Systems (CPS) relies on a number of analysis tools to verify critical properties. The Architecture Analysis and Design Language (AADL) standard provides a common architectural model to which multiple CPS analyses can be applied. Unfortunately, interaction between these analyses can invalidate their results. In this paper we present ACTIVE, a tool developed within the OSATE/AADL infrastructure to solve this problem. We analyze the problems that occur when multiple analyses are applied to an AADL model and how these problems invalidate analysis results. Interactions between analyses, implemented as OSATE plugins, are formally described in ACTIVE in order to enable automatic verification. In particular, these interactions are captured in an analysis contract consisting of inputs, outputs, assumptions, and guarantees. The inputs and outputs help determine the correct order of execution of the plugins. Assumptions capture the conditions that must be valid in order to execute an analysis plugin, while guarantees are conditions that are expected to be valid afterwards. ACTIVE allows the use of any generic verification tool (e. g., a model checker) to validate these conditions. To coordinate these activities our tool uses two components: ACTIVE EXECUTER and ACTIVE VERIFIER. ACTIVE EXECUTER invokes the analysis plugins in the required order and uses ACTIVE VERIFIER to check assumptions and guarantees. ACTIVE VERIFIER identifies and executes the verification tool that needs to be invoked based on the target formula. Together, they ensure that plugins are always executed in the correct order and under the correct conditions, guaranteeing correct results. To the best of our knowledge, ACTIVE is the first extensible framework that integrates independently-developed analysis plugins ensuring provably-correct interactions.

Abstract: Developing cyber-physical systems involves creating systems with properties from multiple domains, e. g., timing, logical correctness, thermal resilience, aerodynamics, and mechanical stress. In today/s industrial practice, multiple analyses are used to obtain and verify such properties. Unfortunately, given that these analyses originate from different scientific domains, they abstract away interactions among themselves, risking the invalidation of their results. Specifically, one challenge is to ensure that an analysis is never applied to a model that violates its assumptions. Since such violation can originate from the updating of the model by another analysis, analyses must be executed in the correct order. Another challenge is to do this soundly and scalably over models of realistic complexity and diverse set of analyses. To address these challenges, we develop an analysis integration approach that uses contracts to specify dependencies between analyses, determine their correct orders of application, and specify and verify applicability conditions across multiple domains. We present an implementation of our approach, and demonstrate its effectiveness, extensibility, and scalability.

Abstract: Self-adaptive systems have the ability to adapt their behavior to dynamic operation conditions. In reaction to changes in the environment, these systems determine the appropriate corrective actions based in part on information about which action will have the best impact on the system. Existing models used to describe the impact of adaptations are either unable to capture the underlying uncertainty and variability of such dynamic environments, or are not compositional and described at a level of abstraction too low to scale in terms of specification effort required for non-trivial systems. In this paper, we address these shortcomings by describing an approach to the specification of impact models based on architectural system descriptions, which at the same time allows us to represent both variability and uncertainty in the outcome of adaptations, hence improving the selection of the best corrective action. The core of our approach is an impact model language equipped with a formal semantics defined in terms of Discrete Time Markov Chains. To validate our approach, we show how employing our language can improve the accuracy of predictions used for decision-making in the Rainbow framework for architecture-based self-adaptation.

Abstract: Architecture-based self-adaptation is considered as a promising approach to drive down the development and opera-tion costs of complex software systems operating in ever changing environments. However, there is still a lack of evidence supporting the arguments for the beneficial impact of architecture-based self-adaptation on resilience with respect to other customary approaches, such as embedded code-based adaptation. In this paper, we report on an empirical study about the impact on resilience of incorporating architecture-based self-adaptation in an industrial middleware used to collect data in highly populated networks of devices. To this end, we compare the results of resilience evaluation between the original version of the middleware, in which adaptation mechanisms are embedded at the code-level, and a modifi ed version of that middleware in which the adaptation mechanisms are implemented using Rainbow, a framework for architecture-based self-adaptation. Our results show improved levels of resilience in architecture-based compared to embedded code-based self-adaptation.

Abstract: Availability is an increasingly important quality for today's software-based systems and it has been successfully addressed by the use of closed-loop control systems in self-adaptive systems. Probes are inserted into a running system to obtain information and the information is fed to a controller that, through provided interfaces, acts on the system to alter its behavior. When a failure is detected, pinpointing the source of the failure is a critical step for a repair action. However, information obtained from a running system is commonly incomplete due to probing costs or unavailability of probes. In this paper we address the problem of fault localization in the presence of incomplete system monitoring. We may not be able to directly observe a component but we may be able to infer its health state. We provide formal criteria to determine when health states of unobservable components can be inferred and establish formal theoretical bounds for accuracy when using any spectrum-based fault localization algorithm.

Abstract: Although different approaches to decision-making in self-adaptive systems have shown their effectiveness in the past by factoring in predictions about the system and its environment (e. g., resource availability), no proposal considers the latency associated with the execution of tactics upon the target system. However, different adaptation tactics can take different amounts of time until their eff ects can be observed. In reactive adaptation, ignoring adaptation tactic latency can lead to suboptimal adaptation decisions (e. g., activating a server that takes more time to boot than the transient spike in traffic that triggered its activation). In proactive adaptation, taking adaptation latency into account is necessary to get the system into the desired state to deal with an upcoming situation. In this paper, we introduce a formal analysis technique based on model checking of stochastic multiplayer games (SMGs) that enables us to quantify the potential benefi ts of employing different types of algorithms for self-adaptation. In particular, we apply this technique to show the potential benefi t of considering adaptation tactic latency in proactive adaptation algorithms. Our results show that factoring in tactic latency in decision making improves the outcome of adaptation. We also present an algorithm to do proactive adaptation that considers tactic latency, and show that it achieves higher utility than an algorithm that under the assumption of no latency is optimal.

Abstract: Security features are often hardwired into software applications, making it difficult to adapt security responses to reflect changes in runtime context and new attacks. In prior work, we proposed the idea of architecture-based self-protection as a way of separating adaptation logic from application logic and providing a global perspective for reasoning about security adaptations in the context of other business goals. In this paper, we present an approach, based on this idea, for combating denial-of-service (DoS) attacks. Our approach allows DoS-related tactics to be composed into more sophisticated mitigation strategies that encapsulate possible responses to a security problem. Then, utility-based reasoning can be used to consider diff erent business contexts and qualities. We describe how this approach forms the underpinnings of a scientific approach to self-protection, allowing us to reason about how to make the best choice of mitigation at runtime. Moreover, we also show how formal analysis can be used to determine whether the mitigations cover the range of conditions the system is likely to encounter, and the effect of mitigations on other quality attributes of the system. We evaluate the approach using the Rainbow self-adaptive framework and show how Rainbow chooses DoS mitigation tactics that are sensitive to diff erent business contexts.

Abstract: In many scientific fields, simulations and analyses require compositions of computational entities such as web services, programs, and applications. In such fields, users may want various trade-offs between different qualities. Examples include: (i) performing a quick approximation vs. an accurate, but slower, experiment, (ii) using local slower execution environments vs. remote, but advanced, computing facilities, (iii) using quicker approximation algorithms vs. computationally expensive algorithms with smaller data. However, such trade-offs are difficult to make as many such decisions today are either (a) wired into a fixed configuration and cannot be changed, or (b) require detailed systems knowledge and experimentation to determine what configuration to use. In this paper we propose an approach that uses architectural models coupled with automated design space generation for making fidelity and timeliness trade-offs. We illustrate this approach through an example in the intelligence analysis domain.

Abstract: Over the past two and a half decades software architecture has emerged as an important subfield of software engineering. During that time there has been considerable progress in developing the technological and methodological base for treating architectural design as an engineering discipline. However, much still remains to be done to achieve that. Moreover, the changing face of technology raises a number of challenges for software architecture. This travelogue recounts the history of the field, its current state of practice and research, and speculates on some of the important emerging trends, challenges, and aspirations

Abstract: Ozone Widget Framework (OWF) is an event-based web platform for lightweight integration of widget applications. This technical report presents a formal model of OWF’s widget composition mechanism. First, we present a detailed description of Ozone’s end user composition mechanism. Then, we describe our architectural modeling approach and its value for analysis of OWF widget compositions. We go through the process of creating an architectural style to represent assemblies of Ozone widgets, reviewing modeling decision points and style alternatives.

Abstract: The fundamental premise behind Moving Target Defense (MTD) is to create a dynamic and shifting system that is more difficult to attack than a static system because a constantly changing attack surface at least reduces the chance of an attacker finding and exploiting the weakness. However, MTD approaches are typically chosen without regard to other qualities of the system, such as performance or cost. This report explores the use of self-adaptive systems, in particular those based on the architecture of the running system. A systems software architecture can be used to trade off different quality dimensions of the system. In particular, this report describes the first steps in reasoning formally about MTD approaches, and elevating this reasoning to an architectural level, along three thrusts: (1) creating an initial catalog of MTD tactics that can be used at the architectural level, along with the impacts on security and other quality concerns, (2) using this information to inform proactive self-adaptation that uses predictions of tactic duration to improve the self-adaptation, and (3) using stochastic multiplayer games to verify the the behavior of a variety of MTD scenarios, from uninformed to predictive-reactive. This work is applied in the context of the Rainbow self-adaptive framework.