Expeditions in Computer Augmented Program Engineering (NSF Expeditions)
The goal of ExCAPE is to transform the way programmers develop software by advancing the theory and practice of software synthesis. In the proposed paradigm, a programmer can express insights through a variety of forms such as incomplete programs, example behaviors, and high-level requirements, and the synthesis tool generates the implementation relying on powerful analysis algorithms and programmer collaboration. The ExCAPE plan is to produce a range of design tools; that let end users program robots by demonstrating example behaviors, and that provide smart assistance for expert programmers to meet challenges in multicore programming.
Greater Philadelphia Innovation Cluster (GPIC) for Energy Efficient Buildings (DoE HUB)
The Greater Philadelphia Innovation Cluster (GPIC) for Energy Efficient Buildings received $129 million from the Federal Government's Energy Regional Innovation Cluster (E-RIC) Initiative. The award included $122 million from the U.S. DOE to create the GPIC/HUB to develop innovative energy efficient building technologies, designs and systems. The GPIC/HUB goal is to transform the commercial building retrofit and new construction processes into a systems-delivery industry, and demonstrate building operational energy savings of 50% by 2013-2015 in a scalable, repeatable and cost effective manner across a broad building stock, while preserving workplace quality.
Heterogeneous Unmanned Networked Teams (ONR HUNT)
The grand challenge for this multi-university project is to push the state-of-the-art in complex, time-critical mission planning and execution for large numbers of heterogeneous vehicles collaborating with humans. Sophisticated cooperation among intelligent biological organisms, including humans, will offer critical insight and solution templates for many hard engineering problems. To meet this challenge, we have a assembled an interdisciplinary team of leading researchers who have pioneered work in artificial intelligence, vehicle control and robotics, cognitive psychology and human factors, biology, and political economics. This multi-university project is led by the University of Pennsylvania and will be performed in collaboration with the Georgia Institute of Technology, the University of California at Berkeley, medicalnd Arizona State University.
Quantitative Analysis and Design of Control Networks (NSF CPS)
Control networks are wireless substrates for industrial automation control, such as the WirelessHART and Honeywell's OneWireless, and have fundamental differences over their sensor network counterparts as they also include actuation and the physical dynamics. The approach of the project is based on using time-triggered communication and computation as a unifying abstraction for understanding control networks. Time-triggered architectures enable the natural integration of communication, computation, and physical aspects of control networks as switched control systems. The time-triggered abstraction will serve for addressing the following interrelated themes: Optimal Schedules via Quantitative Automata, Quantitative Analysis and Design of Control Networks: Wireless Protocols for Optimal Control: Quantitative Trust Management for Control Networks. Our results will be integrated into control networks that are compatible with both WirelessHART and OneWireless specifications.
Situation undersanding bot through language and environment (ARO MURI)
This multi-university project brings together experts in linguistics, computational linguistics, artificial intelligence, machine learning, and robotics with the goal of developing a language for communication between humans and robots, where robots are responding to a changing environment and reporting on the relevant aspects of those changes. We will develop a broad range of concepts, which will ultimately enable designers to develop powerful communication methods between robots and humans, enabling humans to communicate goals and intentions as well as direct commands to robots in a natural, effective way. This multi-university project is led by the University of Pennsylvania and will be performed in collaboration with the University of Massachusstts at Amherst and the University of Massachusets at Lowell.
Robust testing by testing robustness of embedded systems (NSF EHS)
In recent years, the idea of the model-based design paradigm is to develop design models and subject them to early analysis, testing, and validation prior to their implementation. Simulation-based testing ensures that a finite number of user-defined system trajectories meet the desired specification. Even though computationally inexpensive simulation is ubiquitous in system design, it suffers from incompleteness, as it is impossible or impractical to test all system trajectories. On the other hand, verification methods enjoy completeness by showing that all system trajectories satisfy the desired property. This project brings together leading experts in embedded control, hybrid systems, and software monitoring and testing to develop the foundations of a modern framework for testing the robustness of embedded hybrid systems. The central idea that this project is centered around is the notion of a robust test, where the robustness of nominal test can be computed and used to infer that a tube of trajectories around the nominal test will yield the same qualitative behavior.
Scalable swarms of autonomous robots and mobile sensors (ARO MURI)
This multi-university project brings together experts in artificial intelligence, control theory, robotics, systems engineering and biology with the goal of understanding swarming behaviors in nature and applications of biologically-inspired models of swarm behaviors to large networked groups of autonomous vehicles. Our main goal is to develop a framework and methodology for the analysis of swarming behavior in biology and the synthesis of bio-inspired swarming behavior for engineered systems. This multi-university project is led by the University of Pennsylvania and will be performed in collaboration with the Massachusets Institute of Technology, the University of California at Berkeley, the University of California at Santa Barbara, and Yale University.
Synthesis of embedded software from hybrid models (NSF EHS)
Despite the proliferation of embedded devices in almost every engineered product, development of embedded software remains a low level, time consuming and error prone process. This is due to the fact that modern programming languages abstract away from time and platform constraints, while correctness of embedded software relies crucially on hard deadlines. This NSF-funded research aims at developing novel model-based design and implementation methodology for synthesizing reliable embedded software. Hybrid systems models, which allow mixing state-machine based discrete control with differential equation based continuous dynamics, are used for design and analysis. The research explores ways of mapping such models to code guided by correctness, modularity and portability issues. Technical challenges include bridging the gap between the platform-independent and timed semantics of the hybrid models and the executable software generated from it. This includes integrating generation of control tasks with scheduling to ensure optimal performance.
Sensor topologies for minimal planning (DARPA SToMP)
The Sensor Topology for Minimal Planning (SToMP) program leverages high-dimensional mathematical insights to create new capabilities that capitalize on emerging opportunities where sensors are miniaturized, pervasive, and coordinated. By developing new mathematical methods and techniques, the program seeks to revolutionize how networked sensors and autonomous agents are analyzed, distributed, and controlled. Of central importance will be a systematic determination and exploitation of minimization of total sensor complexity. More precisely, given a mission having a variety of costs to be optimized (e.g., total number of sensors, network bandwidth, or power consumption) the program seeks to determine solutions that require the least resources with respect to such metrics. Thus, the program aims to derive optimal solutions in that it focuses on implementations that are minimal in terms of reducing the total sensor complexity to the minimal configuration required.
Algorithmic synthesis of embedded controllers (NSF EHS)
Embedded systems require very novel, very challenging specifications that have to deal with synchronization, sequencing, and temporal ordering of different tasks. Mathematically formulating such desired specifications cannot be achieved using traditional mathematical formulations in control theory. On the other hand, computer aided verification has popularized the use of several temporal logics to describe complex specifications. However, the emphasis has been on verification of these properties for purely discrete systems, and not on synthesis for systems with a continuous component. In this research, a novel approach for automatically synthesizing hybrid controllers is pursued in order to satisfy specifications that are expressed in temporal logics. The proposed framework will provide algorithms and tools for the computation of discrete controllers, which by refinement will lead to embedded, hybrid controllers for the original system while providing performance and correctness guarantees.
Multi-robot emergency response (NSF ITR)
This project, in collaboration with the University of Minnesota and the California Institute of Technology, addresses research issues key to an important application of robot teams and information technology (emergency response in hazardous environments for various tasks). The research focuses on the development of methods for team coordination and dynamic distribution of tasks to robots. The project integrates the algorithms with first responder teams, emphasizing realistic scenarios.
Formal analysis and design of hybrid systems (NSF ITR)
High-level design of embedded software requires modeling concepts such as hierarchy, modularity, reuse, compositionality, and object-orientation. In this project we will develop a theory of hierarchical hybrid systems with an accompanying a compositional calculus of refinement. This will be the basis for behavioral interfaces and descriptions of components at different levels of abstractions. For rigorously specifying and evaluating design alternatives and correctness requirements, automated techniques such as model checking are very effective. To apply these techniques for formal analysis of hybrid systems, this research is developing automated schemes for constructing abstractions of hybrid models. The technical directions being pursued include model checking algorithms that exploit hierarchy, algorithms for extracting finite-state approximations using predicate abstraction, counter-example guided refinement of abstractions, property-preserving bisimulation-based reductions of continuous differential equations, and assume-guarantee reasoning. The results of this research are being integrated in software tools for modeling and analysis of hybrid systems. The benefits of the techniques for developing embedded systems with higher assurance for safety and reliability are evaluated in an experimental testbed of multiple, autonomous, mobile robots.
Adaptive coordinated control of intelligent multi-agent teams (ARO MURI)
This multi-university project involves the University of Pennsylvania, the University of California at Berkeley, and Carnegie Mellon University. It focuses on the design and evaluation of the adaptive hierarchical control of mixed autonomous and human operated semi-autonomous teams that deliver high levels of mission reliability despite uncertainty arising from rapidly evolving environments and malicious interference from an intelligent adversary. The design of architectures combining both hierarchical and heterarchical elements, the analytical foundations of interacting hybrid systems, the design of controllers for such systems that are robust against uncertainty, the management of rich sensory information from networked sensors among distributed and mobile teams; and the incorporation of human intervention in a mixed-initiative system are all key areas of our work. Additionally, the novelty of our approach is to explicitly take into account the need to adaptively replan missions to take into account environmental uncertainties and the deliberate malicious actions of a determined adversary. Equipment for this project is supported by an ARO DURIP grant.
Hierarchical abstractions of hybrid systems (NSF CAREER, PECASE)
Hybrid systems provide a theoretical foundation for the modeling, analysis, and design of embedded systems. Hybrid systems naturally combine discrete-event and continuous-time systems in a manner that can capture software logic, physical dynamics, and communication protocols, in a unified modeling framework. The wide applicability of hybrid systems has inspired a great deal of research from both control theory and theoretical computer science. Despite the great success of hybrid systems as a model, the applicability of state-of-the-art analysis and design techniques for hybrid systems has been limited to examples of small size due to complexity. Tthe research and educational agenda of the proposed research focuses on developing the theoretical foundations for the hierarchical decomposition of hybrid systems at various levels of abstraction. The long term goal of the research agenda will address the fundamental problem of given a class of hybrid models, and a class of properties that must be preserved, extract modeling abstractions that preserve the properties of interest. Achieving this goal will consist of first developing robust notions of bi-simulation for purely continuous systems, and then unifying the continuous and discrete notions in a manner that is consistent with the dynamics of hybrid systems.
Model based integration of embedded software (DARPA MoBIES)
The objective of this project is to develop a methodology and toolkit for design of embedded software for multi-agent communicating hybrid systems. The methodology will cover various design stages, including modeling, simulation, analysis, implementation, and monitoring. The methodology will be based on formal modular and hierarchical semantics of multi-agent hybrid systems. The methodology will improve the process for hybrid systems design by decreasing development costs through high-level modeling, by improving reusability by means of modular designs, and by developing more reliable designs with the help of analysis and runtime valiadation.