Abstract: We have developed model-based adaptation, an approach that leverages models of software and its environment to enable automated adaptation. The goal of our approach is to build long-lasting mobile software systems that can effectively adapt to changes in their environment.

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: Cyber-Physical Systems (CPS) integrate computational and physical components. With the digitisation of society and industry and the progressing integration of systems, CPS need to become 'smarter' - in the sense that they can adapt and learn to handle new and unexpected conditions, and improve over time. Smarter CPS present a combination of challenges that existing engineering methods have difficulties addressing: inter-twined digital, physical and social spaces, need for heterogeneous modelling formalisms, demand for context-tied cooperation to achieve system goals, widespread uncertainty and disruptions in changing contexts, inherent human constituents, and continuous encounter with new situations. While approaches have been put forward to deal with some of these challenges, a coherent perspective on engineering smarter CPS is lacking. In this paper, we present six engineering principles for addressing the challenges of smarter CPS. As smarter CPS are software-intensive systems, we approach them from a software engineering perspective with the angle of self-adaptation that offers an effective approach to deal with run-time change. The six principles create an integrated landscape for the engineering and operation of smarter CPS.

Abstract: Self-adaptive software systems rely on planning to make adaptation decisions autonomously. Planning is required to produce high-quality adaptation plans in a timely manner; however, quality and timeliness of planning are conflicting in nature. This conflict can be reconciled with hybrid planning, which can combine reactive planning (to quickly provide an emergency response) with deliberative planning that take time but determine a higher-quality plan. While often effective, reactive planning sometimes risks making the situation worse. Hence, a challenge in hybrid planning is to decide whether to invoke reactive planning until the deliberative planning is ready with a high-quality plan. To make this decision, this paper proposes a novel learning-based approach. We demonstrate that this learning-based approach outperforms existing techniques that are based on specifying fixed conditions to invoke reactive planning in two domains: enterprise cloud systems and unmanned aerial vehicles.

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: Approaches to self-adaptation face a fundamental trade-off between quality and timeliness in decision-making. Due to this trade-off, designers of self-adaptive systems often have to find a fixed and suboptimal compromise between these two requirements. Recent work has proposed the hybrid planning approach that can resolve this trade-off dynamically and potentially in an optimal way. The promise of hybrid planning is to combine multiple planners at run time to produce adaptation plans of the highest quality within given time constraints. However, since decision-making approaches are complex and diverse, the problem of combining them is even more difficult, and no frameworks for hybrid planning. This paper makes an important step in simplifying the problem of hybrid planning by formalizing it and decomposing it into four simpler subproblems. These formalizations will serve as a foundation for creating and evaluating engineering solutions to the hybrid planning problem.

Abstract: Recent research in embedded and cyber-physical systems has developed theories and tools for integration of heterogeneous components and models. These efforts, although important, are insufficient for high-quality and error-free systems integration since inconsistencies between system elements may stem from factors not directly represented in models (e.g., analysis tools and expert disagreements). Therefore, we need to broaden our perspective on integration, and devise approaches in three novel directions of integration: modeling methods, data sets, and humans. This paper summarizes the latest advances, and discusses those directions and associated challenges in integration for cyber-physical systems.

Abstract: Designing secure cyber-physical systems (CPS) is a particularly difficult task since security vulnerabilities stem not only from traditional cybersecurity concerns, but also physical ones as well. Many of the standard methods for CPS design make strong and unverified assumptions about the trustworthiness of physical devices, such as sensors. When these assumptions are violated, subtle inter-domain vulnerabilities are introduced into the system model. In this paper we propose to use formal specification of analysis contracts to expose security assumptions and guarantees of analyses from reliability, control, and sensor security domains. We show that this specification allows us to determine where these assumptions are violated or ignore important failure modes that open the door to malicious attacks. We demonstrate how this approach can help discover and prevent vulnerabilities in a self-driving car example.

Abstract: Rigorous engineering of safety-critical Cyber- Physical Systems (CPS) requires integration of heterogeneous modeling methods from different disciplines. It is often necessary to view this integration from the perspective of analyses – algorithms that read and change models. Although analytic integration supports formal contract-based verification of model evolution, it suffers from the limitation of analytic dependency loops. Dependency loops between analyses cannot be resolved based on the existing contract-based verification. This paper makes a step towards using rich architectural description to resolve circular analytic dependencies. We characterize the dependency loop problem and discuss three algorithmic approaches to resolving such loops: analysis iteration, constraint solving, and genetic search. These approaches take advantage of information in multi-view architectures to resolve analytic dependency loops.

Abstract: Modern cyber-physical systems interact closely with continuous physical processes like kinematic movement. Software component frameworks do not provide an explicit way to represent or reason about these processes. Meanwhile, hybrid program models have been successful in proving critical properties of discrete-continuous systems. These programs deal with diverse aspects of a cyber-physical system such as controller decisions, component communication protocols, and mechanical dynamics, requiring several programs to address the variation. However, currently these aspects are often intertwined in mostly monolithic hybrid programs, which are difficult to understand, change, and organize. These issues can be addressed by component-based engineering, making hybrid modeling more practical. This paper lays the foundation for using architectural models to provide component-based benefits to developing hybrid programs. We build formal architectural abstractions of hybrid programs and formulas, enabling analysis of hybrid programs at the component level, reusing parts of hybrid programs, and automatic transformation from views into hybrid programs and formulas. Our approach is evaluated in the context of a robotic collision avoidance case study.

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: Within an increasing number of domains an important emerging need is the ability for technically naive users to compose computational elements into novel configurations. Examples include astronomers who create new analysis pipelines to process telescopic data, intelligence analysts who must process diverse sources of unstructured text to discover socio-technical trends, and medical researchers who have to process brain image data in new ways to understand disease pathways. Creating such compositions today typically requires low-level technical expertise, limiting the use of computational methods and increasing the cost of using them. In this paper we describe an approach -- which we term end-user architecting -- that exploits the similarity between such compositional activities and those of software architects. Drawing on the rich heritage of software architecture languages, methods, and tools, we show how those techniques can be adapted to support end users in composing rich computational systems through domain-specific compositional paradigms and component repositories, without requiring that they have knowledge of the low-level implementation details of the components or the compositional infrastructure. Further, we outline a set of open research challenges that the area of end-user architecting raises.

Abstract: Cyber-physical systems (CPS) incorporate digital (cyber) and mechanical (physical) elements that interact in complex ways. Many safety-critical CPS, such as autonomous vehicles and drones, are becoming increasingly widespread and hence demand rigorous quality assurance. To this end, CPS engineering relies on modeling methods, which use models to represent the system and design-time analyses to interpret/change the models. Coming from diverse scientific and engineering fields, these modeling methods are difficult to combine, or integrate, due to implicit relations and dependencies between them. CPS failures can lead to substantial damage or loss of life, and are often due to two key integration challenges: (i) inconsistencies between models — contradictions in models that do not add up to a cohesive design, and (ii) incorrect interactions of analyses — analyses performed out-of-order and in mismatched contexts, leading to erroneous analysis outputs. This thesis presents a novel approach to detect and prevent integration issues between CPS modeling methods during the design phase. To detect inconsistencies between models, the approach allows engineers to specify integration properties — quantified logical statements that relate elements of multiple models — in the Integration Property Language (IPL). IPL statements describe verifiable conditions that are equivalent to an absence of inconsistencies. To interface with the models, IPL relies on integration abstractions — simplified representations of models for integration purposes. This thesis proposes two abstractions: views (annotated component-and-connector models, inspired by software architecture) and behavioral properties (expressions in model-specific property languages, such as the linear temporal logic). Combining these abstractions lets engineers relate model structure and behavior in IPL statements. To ensure correct interactions of analyses, I introduce analysis contracts — a lightweight specification that captures inputs, outputs, assumptions, and guarantees for each analysis, in terms of the integration abstractions. Given these contracts, an analysis execution platform performs analyses in the order of their dependencies, and only in the contexts that guarantee correct outputs. My approach to integration was validated on four case studies of CPS modeling methods in different systems: energy-aware planning in a mobile robot, collision avoidance in a mobile robot, thread/battery scheduling in a quadrotor, and reliable/ secure sensing in an autonomous vehicle. This validation has shown that the approach can find safety-critical errors by specifying expressive integration properties and soundly checking them within practical constraints — all while being customizable to heterogeneous models, analyses, and domains.

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: Planning approaches in self-adaptation face the fundamental trade-off between quality and timeliness of adaptation plans. Due to this trade-off, today designers often have to compromise between a planning approach that is quick to find a plan and an approach that is slow but finds a quality plan. To deal with this trade-off, researchers have proposed a hybrid planning approach that combines more than one planning approaches to find a balance between quality and timeliness. However, the diversity of planning approaches makes the problem of hybrid planning complex and multi-faceted. This paper advances the theory of hybrid planning by formalizing the central concepts and four subproblems of hybrid planning. This formalization can serve as a foundation for not only understanding and comparing existing hybrid planners, but also for developing new hybrid planners in the future. Moreover, to illustrate practicality of the formal model, the paper uses it to analyze two hybrid planning instantiations that have shown to effective in their respective contexts. Furthermore, grounded on the formal model, the paper formalizes explicit/implicit assumptions about these instantiations that must hold for them to be sound.