I received my Ph.D. in Mechanical Engineering from the California Institute of Technology in June 2013. Before that, I graduated from Harvard University with my S.B. in Mechanical Engineering and Material Science in 2007. My dissertation focused on using formal methods and specification languages in the design and analysis of large-scale, complex, distributed sensing, actuation, and control systems with an emphasis on correct-by-construction control synthesis.
My research interests comprise the areas of control and dynamical systems, optimization, and formal methods with applications in autonomy, planning, and system identification. In particular, I am interested in developing and designing robust cyber-physical systems that are capable of performing high-level, complex goals while reacting to dynamic and possibly adversarial environments. The overall research goal is to provide provably correct results through the use of three key aspects from my research: (1) rigorous theory drawn from mathematics, controls, and computer science (e.g., graph theory and formal methods); (2) computational tractability and how complexity may be overcome through decompositions and interface contracts; and (3) applications to real-world/industry problems (e.g., smart-grid, autonomous vehicles, security of cyber-physical systems).
Distributed Sense and Control
Distributed sense and control systems combining large numbers of heterogeneous components have wide-reaching applications, from energy management (power grid monitoring and traffic control) to autonomous vehicles and aircraft. The unexpected interactions of a large number of interdependent subsystems in the design of such large-scale applications means a greater emphasis must be made on design methodologies that can provide guarantees on behavior and execution. My dissertation research revolves around the design and analysis of large-scale, complex, distributed sensing, actuation, and control systems with an emphasis on correct-by-construction control synthesis from formal specifications. Using an aircraft electric power system as a case example, I have demonstrated how a complete design methodology can be used from beginning optimal design of base topologies to formalization of requirements to automatic synthesis of reactive control protocols.
Temporal Logic Planning
Temporal logic planning is at the intersection of formal methods, automata theory, and control theory. It provides a hierarchical framework for synthesizing controllers based on a system’s intended behavior requirements. Reactive discrete planners are implemented at the high-level while continuous controllers, which implement the discrete plan, are used at the low-level. In my recent work, I have extended the temporal logic planning framework in two ways and applied these ideas to the application domain of aircraft vehicle management systems. The first extension has been the conversion of high-level system requirements into a formal specification language. I have created an aircraft electric power system domain-specific language that can be used, in conjunction with its associated program code, to automatically convert common domain-specific requirements into a formal specification language compatible with current synthesis solvers. The second extension has been developing a formalism for synthesizing correct-by-construction timed and untimed protocols from temporal logic specifications for aircraft electric power systems. I have proposed a framework for writing specifications in a compact manner. Furthermore, I have utilized previous work on distributed synthesis to reduce computational complexity and enhance design modularity for these large-scale, complex systems.
Real-Time Flight Planning Simulation Software for Unmanned Aircraft Systems/Millennium Engineering and Integration
This project aims to develop and demonstrate a real-time flight simulation tool that integrates mission planning, ground command/control, onboard situational awareness, and onboard re-planning for unmanned aircraft vehicles (UAV). The tool will aid in the assessment of potential flight-safety hardware subsystems and embedded algorithmic solutions to enable operation of UAVs within the National Airspace (NAS) and uncontrolled urban airspace.
Electric VTOL Real-Time HIL Test Environment/HopFlyt
This project develops preliminary flight control logic in a simulated environment for use in flight testing a proof of concept UAV that aims to “hop” over traffic for distances up to 30 miles, carrying up to three passengers at a time. The project envisions reducing the 90-minute drive from Baltimore to Washington, D.C. during rush hour to just 15 minutes.
Planning and Metareasoning for Multi-agent Systems with Variable Communication Availability/AFRL
Joint project with Jeffrey Hermann (ME), Shapour Azarm (ME), and Michael Otte (AE). We generate knowledge about multi-agent planning and metareasoning based on dynamic tasking and communication availability. The proposed research includes two key areas: (1) develop, understand, and characterize the performance of hybrid centralized/decentralized multi-agent planning methods with dynamic tasking for different levels of communication availability; and (2) develop, analyze, and compare metareasoning techniques that enable autonomous agents in multi-agent systems to select the most appropriate planning method based on the real-time needs for tasking (including task removal during execution) and observations of the current level of communication availability.
Route Planning With Complex Geometries/NAVAIR
We explore a methodology for training recurrent neural networks in replicating path planning solutions from optimization problems. Training data is generated from a kino-dynamic rapidly-exploring random tree, from which a recurrent neural network is trained upon to produce the state path through fixed time-step execution. Path-tracking controllers are formulated to follow the path generated by the network alongside the use of local potential functions to mitigate minor constraint violations. The control signal from such a controller should mimic that of the optimized solution, but can be generated orders of magnitude faster than the slower planning solutions.
The Student Unmanned Aircraft Systems (SUAS) Competition, aimed at stimulating and fostering interest in unmanned air systems, technologies and careers, focuses on engaging students in a challenging mission. It requires the design, integration, and demonstration of a system capable of conducting air operations, which include autonomous flight, navigation of a specified course, and use of onboard payload sensors.
Competitive autonomous drone racing is an engineering and computer science challenge that requires an understanding of computer vision, the ability to develop algorithms that incorporate the gate detection, and programming logic for the drone to understand when it has completed tasks. Students compete annually at the IEEE International Conference on Intelligent Robots and Systems (IROS).
Robust Semi-Autonomous Swarm Tactics for Situational Awareness in Uncertain Environments/DARPA
Joint Project with Ming Lin (CS), Dinesh Manocha (CS), and Michael Otte (AE). This work creates novel and useful semi-autonomous aerial swarm tactics for the surveillanceof a hostile urban environment with uncertainty by enabling a 3D interactive model of the urbanenvironment to be created and continually updated with visual and geometric data captured bythe swarm. These tactics will be robust with respect to uncertainty in the environment as wellas sensor noise. This will enable a single human user to have real-time battlefield situationalawareness within dynamic hostile environments. While current use of unmanned systems requiresmultiple humans to operate a single vehicle, this capability would allow a single operator to controlmultiple vehicles.
Mission planning for autonomous systems in dynamic environments using open-source autopilots/NAVAIR
This project investigates the integration and certification of open source autopilots in unmanned aerial vehicles using motion planning as a formal framework. The objective is for UMD to develop autopilot architectures and mission planning algorithms using open-source software and off-the-shelf autopilots (e.g., Navio2).
Non-Cooperative Detect and Avoid Capabilities for UAS Platforms/Lockheed Martin
This project leverages University of Maryland research in the areas of UAS detection for counter-UAS applications and autonomous vehicle path and trajectory planning to address non-cooperative detect and avoid capability for UAS systems.
Cybersecurity Detection for UAVs/MITRE
The main goal of this project is to provide theoretical guarantees on the ability to estimate and recover from security threats to cyberphysical systems. We aim to develop a simulation and hardware testbed in which the proposed mathematical framework can be used to detect, assess, and recover from threats (both internal and external).
Please feel free to email about preprints.
- Estefany Carrillo, PhD candidate, AE
- Zijie Lin, PhD candidate, ECE
- Tori Hawkins, PhD Candidate, AE
- Guangyao Shi, PhD Candidate, ECE
- Donald Costello, PhD Candidate, ME
- Senthil Adarsh, MS, Systems Engineering
- Derek Thompson, MS, Aerospace Engineering
- Ed Carney, MS, Aerospace Engineering
- Suyash Yeotikar, MS, Robotics
- Joshua Shaffer, MS 2019, Aerospace Engineering
- Vincenz Frenzel, MS 2019, Aerospace Engineering (Visiting Scholar)
- Edward Mortimer, BS/MS 2019, Aerospace Engineering (Visiting Scholar)
- Andrew Poissant, BS/MS 2018, Systems Engineering
- Matthew Solomon, MS 2016, Aerospace Engineering
- Niloofar Shadab, MS 2016, Systems Engineering
- Bao Zhang, MS 2014, Systems Engineering Engineering
FALL: ENAE 380 Flight Software Systems
Avionics using advanced sensor and computing technologies are at the heart of every modern aerospace vehicle. Advanced software systems improve cockpit safety and enable unmanned and deep-space missions. Object-oriented programming and software engineering concepts required to design and build complex ﬂight software systems will be discussed. Other discussions include software validation, veriﬁcation, real-time performance analysis to assess ﬂight software system reliability and robustness; human-machine interfaces designed for piloted systems; automatic onboard data acquisition and decision-making for unmanned air and space vehicles.
SPRING: ENES489p Special Topics in Engineering (Hands-On Systems Engineering Projects)
This hands-on design projects course will expose senior-level undergraduate and graduate-level students from all areas of engineering to exciting career opportunities in the systems engineering field. Students will be introduced to the technical aspects of systems engineering practice through team-based project development and a systematic step-by-step procedure for product development that includes working with a real-world customer to define operations concepts, requirements gathering and organization, synthesis of models of system behavior and system structure, functional allocation to create system design alternatives, formal assessment of design alternatives through tradeoff analysis, and established approaches to testing and validation/verification.
SPRING: ENSE 698B Applied Formal Methods
This course introduces best practices for the application of formal methods, a set of mathematically rigorous techniques for the formal specification, validation, and verification of safety-critical systems, of which aircraft and spacecraft are the prime examples. The course explores tools, techniques, and applications of formal methods, focusing on aerospace and robotic domains. Students examine the latest research to gain an understanding of the current state of the art, including the capabilities and limitations of applying formal methods for systems analysis.
3180 Glenn L. Martin Building
College Park, MD 20742
Phone: +1 301 405 1133