An official website of the United States government
In this paper, we introduce the design and implementation of a low-cost, small-scale autonomous vehicle equipped with an onboard computer, a camera, a Lidar, and some other accessories. We implement various autonomous driving-related modules including mapping and localization, object detection, obstacle avoidance, and path planning. In order to better test the system, we focus on the autonomous parking scenario. In this scenario, the vehicle is able to move from an appointed start point to the desired parking lot autonomously by following a path planned by the hybrid A* algorithm. The vehicle is able to detect objects and avoid obstacles on its path and achieve autonomous parking.
more »
« less
Automated Synthesis of Secure Platform Mappings
System development often involves decisions about how a high-level design is to be implemented using primitives from a low-level platform. Certain decisions, however, may introduce undesirable behavior into the resulting implementation, possibly leading to a violation of a desired property that has already been established at the design level. In this paper, we introduce the problem of synthesizing a property-preserving platform mapping: synthesize a set of implementation decisions ensuring that a desired property is preserved from a high-level design into a low-level platform implementation. We formalize this synthesis problem and propose a technique for generating a mapping based on symbolic constraint search. We describe our prototype implementation, and two real-world case studies demonstrating the applicability of our technique to the synthesis of secure mappings for the popular web authorization protocols OAuth 1.0 and 2.0.
more »
« less
- Award ID(s):
- 1801546
- PAR ID:
- 10095152
- Date Published:
- Journal Name:
- Computer Aided Verification (CAV)
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Contact-based decision and planning methods are becoming increasingly important to endow higher levels of autonomy for legged robots. Formal synthesis methods derived from symbolic systems have great potential for reasoning about high-level locomotion decisions and achieving complex maneuvering behaviors with correctness guarantees. This study takes a first step toward formally devising an architecture composed of task planning and control of whole-body dynamic locomotion behaviors in constrained and dynamically changing environments. At the high level, we formulate a two-player temporal logic game between the multi-limb locomotion planner and its dynamic environment to synthesize a winning strategy that delivers symbolic locomotion actions. These locomotion actions satisfy the desired high-level task specifications expressed in a fragment of temporal logic. Those actions are sent to a robust finite transition system that synthesizes a locomotion controller that fulfills state reachability constraints. This controller is further executed via a low-level motion planner that generates feasible locomotion trajectories. We construct a set of dynamic locomotion models for legged robots to serve as a template library for handling diverse environmental events. We devise a replanning strategy that takes into consideration sudden environmental changes or large state disturbances to increase the robustness of the resulting locomotion behaviors. We formally prove the correctness of the layered locomotion framework guaranteeing a robust implementation by the motion planning layer. Simulations of reactive locomotion behaviors in diverse environments indicate that our framework has the potential to serve as a theoretical foundation for intelligent locomotion behaviors.more » « less
-
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.more » « less
-
null (Ed.)Many techniques were proposed for detecting software misconfigurations in cloud systems and for diagnosing unintended behavior caused by such misconfigurations. Detection and diagnosis are steps in the right direction: misconfigurations cause many costly failures and severe performance issues. But, we argue that continued focus on detection and diagnosis is symptomatic of a more serious problem: configuration design and implementation are not yet first-class software engineering endeavors in cloud systems. Little is known about how and why developers evolve configuration design and implementation, and the challenges that they face in doing so. This paper presents a source-code level study of the evolution of configuration design and implementation in cloud systems. Our goal is to understand the rationale and developer practices for revising initial configuration design/implementation decisions, especially in response to consequences of misconfigurations. To this end, we studied 1178 configuration-related commits from a 2.5 year version-control history of four large-scale, actively-maintained open-source cloud systems (HDFS, HBase, Spark, and Cassandra). We derive new insights into the software configuration engineering process. Our results motivate new techniques for proactively reducing misconfigurations by improving the configuration design and implementation process in cloud systems. We highlight a number of future research directions.more » « less
-
Abstract System design has been facing the challenges of incorporating complex dependencies between individual entities into design formulations. For example, while the decision-based design framework successfully integrated customer preference modeling into optimal design, the problem was formulated from a single entity’s perspective, and the competition between multiple enterprises was not considered in the formulation. Network science has offered several solutions for studying interdependencies in various system contexts. However, efforts have primarily focused on analysis (i.e., the forward problem). The inverse problem still remains: How can we achieve the desired system-level performance by promoting the formation of targeted relations among local entities? In this study, we answer this question by developing a network-based design framework. This framework uses network representations to characterize and capture dependencies and relations between individual entities in complex systems and integrate these representations into design formulations to find optimal decisions for the desired performance of a system. To demonstrate its utility, we applied this framework to the design for market systems with a case study on vacuum cleaners. The objective is to increase the sales of a vacuum cleaner or its market share by optimizing its design attributes, such as suction power and weight, with the consideration of market competition relations, such as inter-brand triadic competition involving three products from different brands. We solve this problem by integrating an exponential random graph model (ERGM) with a genetic algorithm. The results indicate that the new designs, which consider market competition, can effectively increase the purchase frequency of specific vacuum cleaner models and the proposed network-based design method outperforms traditional design optimization.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
