Abstract: Advances in CAD and CAM have enabled engineers and design teams to digitally design parts with unprecedented ease. Software solutions now come with a range of modules for optimizing designs for performance requirements, generating instructions for manufacturing, and digitally tracking the entire process from design to procurement in the form of product life-cycle management tools. However, existing solutions force design teams and corporations to take a primarily serial approach where manufacturing and procurement decisions are largely contingent on design, rather than being an integral part of the design process. In this work, we propose a new approach to part making where design, manufacturing, and supply chain requirements and resources can be jointly considered and optimized. We present the Generative Manufacturing compiler that accepts as input the following: 1) An engineering part requirements specification that includes quantities such as loads, domain envelope, mass, and compliance, 2) A business part requirements specification that includes production volume, cost, and lead time, 3) Contextual knowledge about the current manufacturing state such as availability of relevant manufacturing equipment, materials, and workforce, both locally and through the supply chain. Based on these factors, the compiler generates and evaluates manufacturing process alternatives and the optimal derivative designs that are implied by each process, and enables a user guided iterative exploration of the design space. As part of our initial implementation of this compiler, we demonstrate the effectiveness of our approach on examples of a cantilever beam problem and a rocket engine mount problem and showcase its utility in creating and selecting optimal solutions according to the requirements and resources.

Abstract: Robotic systems are typically composed of various subsystems, such as localization and navigation, each encompassing numerous configurable components (e. g., selecting different planning algorithms). Once an algorithm has been selected for a component, its associated configuration options must be set to the appropriate values. Configuration options across the system stack interact non-trivially. Finding optimal configurations for highly configurable robots to achieve desired performance poses a significant challenge due to the interactions between configuration options across software and hardware that result in an exponentially large and complex configuration space. These challenges are further compounded by the need for transferability between different environments and robotic platforms. Data efficient optimization algorithms (e. g., Bayesian optimization) have been increasingly employed to automate the tuning of configurable parameters in cyber-physical systems. However, such optimization algorithms converge at later stages, often after exhausting the allocated budget (e. g., optimization steps, allotted time) and lacking transferability. This paper proposes CURE - a method that identifies causally relevant configuration options, enabling the optimization process to operate in a reduced search space, thereby enabling faster optimization of robot performance. CURE abstracts the causal relationships between various configuration options and robot performance objectives by learning a causal model in the source (a low-cost environment such as the Gazebo simulator) and applying the learned knowledge to perform optimization in the target (e. g., Turtlebot 3 physical robot). We demonstrate the effectiveness and transferability of CURE by conducting experiments that involve varying degrees of deployment changes in both physical robots and simulation

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: Component-based robot software frameworks, such as the Robot Operating System (ROS), allow developers to quickly compose and execute systems by focusing on configuring and integrating reusable, off-the-shelf components. However, these components often lack documentation on how to configure and integrate them correctly. Even when documentation exists, its natural language specifications are not enforced, resulting in misconfigurations that lead to unpredictable and potentially dangerous robot behaviors. In this work, we introduce ROSpec, a ROS-tailored domain-specific language designed to specify and verify component configurations and their integration. ROSpec’s design is grounded in ROS domain concepts and informed by a prior empirical study on misconfigurations, allowing the language to provide a usable and expressive way of specifying and detecting misconfigurations. At a high level, ROSpec verifies the correctness of argument and component configurations, ensures the correct integration of components by checking their communication properties, and checks if configurations respect the assumptions and constraints of their deployment context. We demonstrate ROSpec’s ability to specify and verify components by modeling a medium-sized warehouse robot with 19 components, and by manually analyzing, categorizing, and implementing partial specifications for components from a dataset of 182 misconfiguration questions extracted from a robotics Q&A platform.

Abstract: Distributed Denial of Service (DDoS) attacks have grown in complexity, with attackers dynamically adapting their strategies to maximize disruption. Dynamic DDoS adversaries evolve their attacks by changing targets, modifying botnet infrastructure, or altering traffic patterns to evade detection and maintain attack effectiveness. This dynamic nature poses significant challenges for DDoS defense, particularly in developing scalable and robust adaptive systems capable of real-time response. This paper introduces a novel, robust, multilayered defense system called DosSink that integrates detection and mitigation through variational autoencoders (VAE) and actor-critic deep reinforcement learning (DRL). The VAE effectively reduces the feature space which may make the learning intractable and characterizes traffic to estimate the risk score for each flow. At the same time, the DRL agent uses these risk scores to optimize mitigation policies that include traffic limiting, flow redirection, or puzzle-based source verification actions. Feedback from puzzle inquiries refines VAE risk assessments, enhancing detection accuracy. Key innovations of this framework include (1) the VAE's adaptability as an anomaly detector that evolves with DRL actions, avoiding reliance on static rules or predefined thresholds and enhancing the robustness of the overall system adaptation; (2) the separation of traffic characterization (VAE) and decisionmaking (DRL), improving scalability by reducing the state space; and (3) real-time adaptability to evolving attackers' strategies through dynamic collaboration between the VAE and DRL. Our evaluation experiments show that this framework accurately identifies malicious traffic flows, with a true positive rate of over 98% and a false positive rate below 1 %. Moreover, it efficiently learns the optimal mitigation strategy in under 20, 000 episodes across most experimental settings.

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: Component-based architectures in robotics, like the Robot Operating System (ROS), simplify system development by integrating reusable, off-the-shelf components. However, these components often lack sufficient documentation on their use and the architectures they form, leading to architectural misconfigurations. General-purpose Architectural Description Languages (ADLs) effectively provide properties to detect misconfigurations but are burdensome to use, as they require mapping new language-specific concepts to the ROS domain. This work introduces rospec, a novel ADL embedding ROS-specific knowledge to help developers specify and detect architectural misconfigurations. By mapping the language's syntax with ROS concepts, we argue that practitioners can more easily understand and reason about specifications written in the language. We provide an example and compare it with a general-purpose ADL.

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: Successful attacks are nearly inevitable as sophisticated threat actors are committed to inflicting damage, leaving digital and physical destruction in their wakes. As defenders recognize the inevitability of successful attacks, they must change their defense paradigms from only preventing attacks to also weathering the attacks that penetrate first-line defenses. Instead, the systems' abilities to provide functionality should be minimally disrupted while simultaneously containing an attacker. The engineering challenge is to build and operate systems that are resilient to attack, able to adapt to trade off some functionality to preserve trust in more-critical functionality. We refer to this concept as graceful degradation. Defenders would be in a far better position to address the increasingly dire situation confronting them if they had a method and tool to support graceful degradation. However, this requires the ability to reason despite uncertainties at architecture and design time and at run time. Automation can be supported by formal modeling of systems, but it must not be labor-intensive. We propose and develop an approach that directly addresses these challenges. We can architect and operate systems that are better able to weather attacks by automating the evaluation of systems' security properties to enable effective automated graceful degradation of systems in the presence of uncertainty through an approach of formally modeling systems and system behavior at an architectural level of abstraction to explore hypothetical attacks and the systems' abilities to respond. We describe our approach and provide tooling to demonstrate our concept.