Abstract: Although tests are traditionally used as mandatory summative assessments at the end of the instruction period and their purpose is measuring how well a student has learned a given subject, they can also play an important role in formative assessment when they are employed as an instrument to aid in the acquisition and retention of knowledge. This study evaluates the role of tests as weekly formative assessments and investigates the impact of their repetition (i.e., administering the same test more than once) on academic performance of students in a postgraduate formal methods course for professional software engineers. Our hypothesis is that repetition in formative assessments leads to increased academic performance, as well as to an improvement in the effectiveness of gauging student progress. Based on an analysis of data from a population of 194 students that took the course during the period 2013-2017, we report results that point at the validity of our hypothesis.

Abstract: Adaptive systems are expected to adapt to unanticipated run-time events using imperfect information about themselves, their environment, and goals. This entails handling the effects of uncertainties in decision-making, which are not always considered as a first-class concern. This paper contributes a formal analysis technique that explicitly considers uncertainty in sensing when reasoning about the best way to adapt, together with uncertainty reduction mechanisms to improve system utility. We illustrate our approach on a Denial of Service (DoS) attack scenario and present results that demonstrate the benefits of uncertainty-aware decision-making in comparison to using an uncertainty-ignorant approach, both in the presence and absence of uncertainty reduction mechanisms.

Abstract: Self-adaptation improves the resilience of software-intensive systems, enabling them to adapt their structure and behavior to run-time changes (e.g., in workload and resource availability). Many of these approaches reason about the best way of adapting by synthesizing adaptation plans online via planning or model checking tools. This method enables the exploration of a rich solution space, but optimal solutions and other guarantees (e.g., constraint satisfaction) are computationally costly, resulting in long planning times during which changes may invalidate plans. An alternative to online planning involves selecting at run time the adaptation best suited to the current system and environment conditions from among a predefined repertoire of adaptation strategies that capture repair and optimization tasks. This method does not incur run-time overhead but requires additional effort from engineers, who have to specify strategies and lack support to systematically assess their quality. In this article, we present MOSAICO, an approach for offline synthesis of adaptation strategy repertoires that makes a novel use of discrete abstractions of the state space to flexibly adapt extra-functional behavior in a scalable manner. The approach supports making trade-offs: (i) among multiple extra-functional concerns, and (ii) between computation time and adaptation quality (varying abstraction resolution). Our results show a remarkable improvement on system qualities in contrast to manually-specified repertoires. More interestingly, moderate increments in abstraction resolution can lead to pronounced quality improvements, whereas high resolutions yield only negligible improvement over medium resolutions.

Abstract: An emerging trend in the engineering of complex systems is the use of component integration frameworks. Such a framework prescribes an architectural design that permits flexible composition of third-party components into applications. A good example is Sun Microsystems' Enterprise JavaBeans (EJB) framework, which supports object-oriented, distributed, enterprise-level applications, such as account management systems. One problem with frameworks like EJB is that they are documented informally, making it difficult to understand precisely what is provided by the framework, and what is required to use it. We believe formal specification can help, and in this paper show how a formal architectural description language can be used to describe and provide insight into such frameworks.

Abstract: Implicit invocation has become an important architectural style for large-scale system design and evolution. This paper addresses the lack of specification and verification formalisms for such systems. A formal computational model for implicit invocation is presented. We develop a verification framework for implicit invocation that is based on Jones' rely/guarantee reasoning for concurrent systems. The application of the framework is illustrated with several examples. The merits and limitations of the rely/guarantee paradigm in the context of implicit invocation systems are also discussed.

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: Software systems are composed of interacting processes that share data between each other in order to satisfy system properties. When these processes deviate and are unavailable to transmit data—due to events such as software bugs, hardware failures, or security attacks—a resilient system will continue delivering safety-critical services. Identify- ing the processes required to satisfy system properties is not a trivial task as there may exist multiple alternative dataflow paths that each satisfy the property. In this work, we propose a formal modeling and analysis technique to compute the sets of minimal processes required to satisfy dataflow properties. The computation of these sets is reduced to a maximum satisfiability problem via modeling in AlloyMax, a for- mal modeling language that performs bounded model checking. We then present a method to formally define the resilience criteria for a system by constraining the minimal dataflow required under maximum system deviations. The efficacy of this work is then evaluated with four case studies motivated from real-world systems with promising results.

Abstract: Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, LTL learning is the problem of synthesizing a specification, in linear temporal logic (LTL), that evaluates to true over the positive traces and false over the negative ones. In this paper, we propose a new type of LTL learning problem called constrained LTL learning, where the user, in addition to positive and negative examples, is given an option to specify one or more constraints over the properties of the LTL formula to be learned. We demonstrate that the ability to specify these additional constraints significantly increases the range of applications for LTL learning, and also allows efficient generation of LTL formulas that satisfy certain desirable properties (such as minimality). We propose an approach for solving the constrained LTL learning problem through an encoding in first-order relational logic and reduction to an instance of the maximal satisfiability (MaxSAT) problem. An experimental evaluation demonstrates that ATLAS, an implementation of our proposed approach, is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in LTL learning.

Abstract: Cyber-physical systems (CPS) with reinforcement learning (RL)-based controllers are increasingly being deployed in complex phys- ical environments such as autonomous vehicles, the Internet-of-Things (IoT), and smart cities. An important property of a CPS is tolerance; i.e., its ability to function safely under possible disturbances and un- certainties in the actual operation. In this paper, we introduce a new, expressive notion of tolerance that describes how well a controller is ca- pable of satisfying a desired system requirement, specified using Signal Temporal Logic (STL), under possible deviations in the system. Based on this definition, we propose a novel analysis problem, called the tol- erance falsification problem, which involves finding small deviations that result in a violation of the given requirement. We present a novel, two- layer simulation-based analysis framework and a novel search heuristic for finding small tolerance violations. To evaluate our approach, we con- struct a set of benchmark problems where system parameters can be configured to represent different types of uncertainties and disturbances in the system. Our evaluation shows that our falsification approach and heuristic can effectively find small tolerance violations.

Abstract: This paper presents Fortis, a tool for automated, formal analysis and repair of robust discrete systems. Given a system model, an environment model, and a safety property, the tool can be used to automatically compute robustness as the amount of deviations in the environment under which the system can continue to guarantee the property. In addition, Fortis enables automated repair of a given system to improve its robustness against a set of intolerable deviations through a process called robustification. With these techniques, Fortis enables a new process for developing robust-by-design systems. The paper presents the overall design of Fortis as well as the key details behind the robustness analysis and robustification techniques. The applicability and performance of Fortis are illustrated through experimental results over a set of case study systems, including a radiation therapy system, an electronic voting machine, network protocols, and a transportation fare system.

Abstract: The feature interaction problem occurs when two or more independently developed components interact with each other in unanticipated ways, resulting in undesirable system behaviors. Feature interaction problems remain a challenge for emerging domains in cyber-physical systems (CPS), such as the Internet of Things and autonomous drones. Existing techniques for resolving feature interactions take a “winner-takes-all” approach, where one out of the conflicting features is selected as the most desirable one, and the rest are disabled. However, when multiple of the conflicting features fulfill important system requirements, being forced to select one of them can result in an undesirable system outcome. In this paper, we propose a new resolution approach that allows all of the conflicting features to continue to partially fulfill their requirements during the resolution process. In particular, our approach leverages the idea of adaptive requirement weakening, which involves one or more features temporarily weakening their level of performance in order to co-exist with the other features in a consistent manner. Given feature requirements specified in Signal Temporal Logic (STL), we propose an automated method and a runtime architecture for automatically weakening the requirements to resolve a conflict. We demonstrate our approach through case studies on feature interactions in autonomous drones.

Abstract: Modern software systems are deployed in a highly dynamic, uncertain environment. Ideally, a system that is robust should be capable of establishing its most critical requirements even in the presence of possible deviations in the environment. We propose a technique called behavioral robustification, which involves systematically and rigorously improving the robustness of a design against potential deviations. Given behavioral models of a system and its environment, along with a set of user-specified deviations, our robustification method produces a redesign that is capable of satisfying a desired property even when the environment exhibits those deviations. In particular, we describe how the robustification problem can be formulated as a multi- objective optimization problem, where the goal is to restrict the deviating environment from causing a violation of a desired property, while maximizing the amount of existing functionality and minimizing the cost of changes to the original design. We demonstrate the effectiveness of our approach on case studies involving the robustness of an electronic voting machine and safety-critical interfaces.

Abstract: Security attacks present unique challenges to self-adaptive system design due to the adversarial nature of the environment. Game theory approaches have been explored in security to model malicious behaviors and design reliable defense for the system in a mathematically grounded manner. However, modeling the system as a single player, as done in prior works, is insufficient for the system under partial compromise and for the design of fine-grained defensive strategies where the rest of the system with autonomy can cooperate to mitigate the impact of attacks. To deal with such issues, we propose a new self-adaptive framework incorporating Bayesian game theory and model the defender (i.e., the system) at the granularity of components. Under security attacks, the architecture model of the system is translated into a Bayesian multi-player game, where each component is explicitly modeled as an independent player while security attacks are encoded as variant types for the components. The optimal defensive strategy for the system is dynamically computed by solving the pure equilibrium (i.e., adaptation response) to achieve the best possible system utility, improving the resiliency of the system against security attacks. We illustrate our approach using an example involving load balancing and a case study on inter-domain routing.

Abstract: The feature interaction problem arises when two or more independent features interact with each other in an undesirable manner.Feature interactions remain a challenging and important problem in emerging domains of cyber-physical systems (CPS), such as intelligent vehicles, unmanned aerial vehicles (UAVs) and the Internet of Things (IoT), where the outcome of an unexpected interaction may result in a safety failure. Existing approaches to resolving feature interactions rely on priority lists or fixed strategies, but may not be effective in scenarios where none of the competing feature actions are satisfactory with respect to system requirements. This paper proposes a novel synthesis-based approach to resolution, where a conflict among features is resolved by synthesizingan action that best satisfies the specification of desirable system behaviors in the given environmental context. Unlike existing resolution methods,our approach is capable of producing a desirable system outcome even when none of the conflicting actions are satisfactory. The effectiveness of the proposed approach is demonstrated using a case study involving interactions among safety-critical features in an autonomous drone.

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: Many self-adaptive systems benefit from human involvement, where a human operator can provide expertise not available to the system and perform adaptations involving physical changes that cannot be automated. However, a lack of transparency and intelligibility of system goals and the autonomous behaviors enacted to achieve them may hinder a human operator's effort to make such involvement effective. Explanation is sometimes helpful to allow the human to understand why the system is making certain decisions. However, explanations come with costs in terms of, e.g., delayed actions. Hence, it is not always obvious whether explanations will improve the satisfaction of system goals and, if so, when to provide them 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 their impact on a human operator's ability to effectively engage in adaptive actions. We then present a decision-making approach for planning in self-adaptation that leverages a probabilistic reasoning tool to determine when the explanation should be used in an adaptation strategy in order to improve overall system utility. We illustrate our approach in a representative scenario for the application of an adaptive news website in the context of potential denial-of-service attacks.

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: 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 computing systems are often formed by multiple components that interact with each other through the use of shared resources (e.g., CPU, network bandwidth, storage). In this paper, we consider a representative scenario of one such system in the context of an Internet of Things application. The system consists of a network of self-adaptive cameras that share a communication channel, transmitting streams of frames to a central node. The cameras can modify a quality parameter to adapt the amount of information encoded and to affect their bandwidth requirements and usage. A critical design choice for such a system is scheduling channel access, i.e., how to determine the amount of channel capacity that should be used by each of the cameras at any point in time. Two main issues have to be considered for the choice of a bandwidth allocation scheme: (i) camera adaptation and network access scheduling may interfere with one another, (ii) bandwidth distribution should be triggered only when necessary, to limit additional overhead. This paper proposes the first formally verified event-triggered adaptation scheme for bandwidth allocation, designed to minimize additional overhead in the network. Desired properties of the system are verified using model checking. The paper also describes experimental results obtained with an implementation of the scheme.

Abstract: Over the past decade there has been considerable progress in the development of formal methods to improve our confidence in complex systems. Today the use of such methods in certain fields, such as hardware design, or nuclear power control systems, is de rigueur, with commensurate improvements in quality and reliability.

Regrettably, however, the use of formalism in the medical device domain is relatively sparse. This is due in large part to the perceived difficulty of using formal methods by ordinary engineers and domain specialists, and by the lack of training in how best to apply existing tools to solve the problems faced in that domain.

Over the past few years we have been developing educational materials to help bridge this gap. Specifically we have developed a course in formal modeling for practicing engineers. A core component of this effort is a set of exercises drawn from the medical device domain, which are used to

a) show how formal modeling can be used as an effective technique to improve quality and reliability of software-intensive systems

b) provide guidelines on selecting appropriate modeling approaches for the problem at hand

c) give students hands-on experience in modeling and tool-assisted analysis

In this paper we outline our use of medical device challenge problems in achieving these goals. We argue that such exercises (and the underlying concepts) can go a long way towards bridging the gap between theory and practice, and could be used more generally to improve the state of the practice in developing high-confidence systems, in general, and medical devices, in particular.

Abstract: The backbone of many architectures is an architectural style that provides a domain-specific design vocabulary and set of constraints on how that vocabulary can be used. Hence, designing a sound and appropriate architectural style becomes an important and intellectually challenging activity. Unfortunately, although there are numerous tools to help in the analysis of individual architectures, relatively less work has been done on tools to help the style designer. In this paper we show how to map an architectural style, expressed formally in an architectural description language, into a relational model that can be automatically checked for properties such as whether a style is consistent, whether a style satisfies some predicate over the architectural structure, whether two styles are compatible for composition, and whether one style refines another.

Abstract: The High-Level Architecture (HLA) provides a common architecture for distributed modeling and simulation. In its original form, the HLA allows a number of simulations to be joined together into a federation using a single run time infrastructure. Recently there has been an interest in joining multiple such federations together using a mediating unit, called an HLA

Abstract: An increasingly important trend in the engineering of complex systems is the design of component integration standards. Such standards define rules of interaction and shared communication infrastructure that permit composition of systems out of independently-developed parts. A problem with these standards is that it is often difficult to understand exactly what they require and provide, and to analyze them in order to understand their deeper properties. In this paper we use our experience in modeling the High Level Architecture (HLA) for Distributed Simulation to show how one can capture the structured protocol inherent in an integration standard as a formal architectural model that can be analyzed to detect anomalies, race conditions, and deadlocks.

Abstract: A critical issue for complex component-based systems design is the modeling and analysis of architecture. One of the complicating factors in developing architectural models is accounting for systems whose architecture changes dynamically (during run time). This is because dynamic changes to architectural structure may interact in subtle ways with on-going computations of the system.

In this paper we argue that it is possible and valuable to provide a modeling approach that accounts for the interactions between architectural reconfiguration and non-reconfiguration system functionality, while maintaining a separation of concerns between these two aspects of a system. The key to the approach is to use a uniform notation and semantic base for both reconfiguration and steady-state behavior, while at the same time providing syntactic separation between the two. As we will show, this permits us to view the architecture in terms of a set of possible architectural snapshots, each with its own steady-state behavior. Transitions between these snapshots are accounted for by special reconfiguration-triggering events.

Abstract: The HLA RTI is a complex artifact, supporting several classes of interaction (e.g., federation management, object management, time management). A critical challenge in producing an RTI architectural framework (and its associated simulation interface specifications) is to develop confidence that its specification is well-formed and complete. In this paper we describe on-going work in formally modelling the HLA both to document the standard more precisely, as well as to analyze it for anomalies, omissions, inconsistencies, and ambiguities. The technical basis for this work is the use of a formal architectural description language, called Wright, and its accompanying toolset.

Abstract: A critical issue in the design of a professional software engineering degree program is the way in which formal methods are integrated into the curriculum. The approach taken by most programs is to teach formal techniques for software development in a separate course on formal methods. In this paper we detail some of the problems with that approach and describe an alternative in which formal methods are integrated across the curriculum. We illustrate the strengths and weaknesses of this alternative in terms of our experience of using it in the Master of Software Engineering Program at Carnegie Mellon University.

Abstract: Robotics systems are complex component-based systems that can consist of many interacting components. When composing and evolving complex component-based systems, the resulting behavior of component interactions sometimes differs from the developers’ expectations. This can, for example, manifest itself in components indefinitely waiting for a required message that no other component sends, components reaching a deadlock state, or messages getting ignored due to systems being in an incorrect state. These bugs, which we call behavioral architecture composition bugs, are often hard to find because the fault locations are spread throughout many different locations in the system. Model-based analysis is a common technique to identify incorrect behavioral composition of complex, safety-critical systems, such as robotics systems. However, in practice, robotics companies usually do not have any formal models, as models for hundreds of software components is a very costly and often labor-intensive and error-prone process. Behavioral models, which would need to be updated whenever the behavior of the component changes, are especially expensive to create. In this dissertation, I present an approach to automatically infer behavioral models for components of systems based on the Robot Operating System (ROS), the most popular framework for robotics systems, using a combination of static and dynamic analysis by exploiting assumptions about the usage of the ROS framework Application Programming Interface (API) and behavioral idioms. Static analysis looks for architecturally-relevant API calls that implement message sending, handling received messages, sleeping for a periodic interval, and behavioral idioms that implement state-dependent behavior and state transitions. Based on this information, static analysis infers state machine models of architecturally-relevant component behavior. Due to limitations of static analysis, the resulting models are often partial. To complement statically inferred models, I present an approach to instrument the source locations of known unknowns and dynamically observe their values. Then, resulting models will be translated into the common language TLA+/PlusCal used for model-checking. Furthermore, I present a model-based analysis technique to find architecture-misconfiguration bugs in the resulting TLA+ models. Then, I present a technique that automatically generates visual diagrams from the inferred models. Our human study with practicing roboticists and graduate students finds that these diagrams support the understanding of architecturally-relevant component behavior without slowing down participants. This work is a contribution towards making well-proven and powerful but infrequently used methods of model-based analysis more accessible and economical in practice to make robotics systems more reliable and safe

Abstract: Abstract Software systems are designed and implemented with assumptions about the environment. However, once a system is deployed, the actual environment may deviate from its expected behavior, potentially leading to violations of desired properties. Ideally, a system should be robust to continue establishing its most critical requirements even in the presence of possible deviations in the environment. To enable systematic design of robust systems against environmental deviations, this work proposes a rigorous behavioral notion of robustness for software systems. Then, it presents a technique called behavioral robustification, which involves two tactics to systematically and rigorously improve the robustness of a system design against potential deviations.

Specifically, the robustness of a system is defined as the largest set of deviating environmental behaviors under which the system is capable of guaranteeing a desired property. Then, we present an approach to compute robustness based on this definition. On the other hand, the system is not robust against an environment when the environment exhibits deviations causing a violation of the desired property. The robustification method finds a redesign that is capable of satisfying the property under such a deviated environment. In particular, two tactics, namely robustification-by-control and robustification-by-specification-weakening, are introduced. The robustification-by-control tactic formulates the robustification problem as a multi-objective optimization problem with the goal of guaranteeing the desired property while maximally preserving the existing functionality and minimizing the cost of changes to the original design. Then, the specification-weakening tactic is used alongside the control tactic, which allows weakening the property to generate more feasible redesigns that retain more functionality or have a lower cost.

The proposed robustness computation and robustification method are implemented in a tool named Fortis. The applicability and efficiency of these approaches are evaluated through experimental results across five case studies, including a radiation therapy machine, an electronic voting machine, network protocols, a transportation fare system, and an infusion pump machine.

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: The High-Level Architecture (HLA) provides a common architecture for distributed modeling and simulation. In its original form the HLA allows a number of simulations to be joined together into a federation using a single run time infrastructure. Recently there has been an interest in joining multiple such federations together using a mediating unit, called an HLA "bridge." This document presents an in-depth study of the feasibility of an HLA bridge in the context of the current HLA interface specification. The results are summarized on two levels. First, we identify general classes of problems and solutions. Second, we provide a detailed discussion of the desired behavior of selected service protocols in the presence of a bridge federate.

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 theory for one aspect of architectural description: 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: An important goal in software engineering is to describe complex software systems at an architectural level of abstraction. While there are many useful architectural paradigms (pipes, blackboards, etc.) they are typically understood only idiomatically and applied in an ad hoc fashion. We show how a formal model allows us to say precisely what we mean by a software architecture, explore its properties, and systematically describe instances of the architecture. We illustrate the approach using the well-known example of pipe-filter architectures.

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.