Research | Active Research Projects

  • ExCAPE: Expeditions in Computer Augmented Program Engineering
    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.
  • Compositional Real-Time Scheduling Framework
    Real-time systems are ones in which correctness depends not only on logical correctness but also on timeliness. For complex real-time systems, it is necessary to develop them as hierarchical systems with real-time components with resource interfaces. This project is to develop abstraction and composition techniques for resource interface while ensuring compositional analysis.
  • High-Confidence Medical Device Software Systems
    The development and production of medical device software and systems is a critical issue as medical device software is increasingly sophisticated and medical devices are networked. Of particular importance is how to ensure such medical device systems are safe.
  • Assuring the Safety, Security and Reliability of Medical Device Cyber Physical Systems
    The objective of this research is to establish a new development paradigm that enables the effective design, implementation, and certification of medical device cyber-physical systems. The approach is to pursue the following research directions: 1) to support medical device interconnectivity and interoperability with network-enabled control; 2) to apply coordination between medical devices to support emerging clinical scenarios; 3) to close the loop and enable feedback about the condition of the patient to the devices delivering therapy; and 4) to assure safety and effectiveness of interoperating medical devices. Novel design methods and certification techniques will significantly improve patient safety. The introduction of closed-loop scenarios into clinical practice will reduce the burden that caregivers are currently facing and will have the potential of reducing the overall costs of health care.
  • MaC (Run-Time Monitoring and Checking)
    As software becomes large and complex, it becomes more difficult to test or verify the correctness of a system. Continuously monitoring of a running system is a complementary approach to increase the assurance of correct execution, which is known as runtime verification. We have been developed a Monitoring and Checking (MaC) framework to monitor and check running systems against a formal requirement specification.
  • QTM (Quantitative Trust Management)
    Cyber Physical Systems (CPS) consists of many interacting heterogeneous components that are distributed and evolve over time. As our lives depend on CPS, trustiness of CPS is important to ensure safe and correct operation of CPS. Quantitative Trust Management (QTM) provides a dynamic interpretation of authorization policies for access control decisions based on upon evolving reputations of the entities involved.
  • Embedded Virtual Machines for Robust Wireless Control
    To address actuation in closed-loop wireless control systems there is a strong need to re-think the communication architectures and protocols for reliability, coordination and control. EVM is the distributed runtime system that maintains functional (e.g. control law) and para-functional invariants (e.g. timeliness, fault-tolerance) across physical node boundaries given an unreliable wireless substrate.
  • 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.
  • Platforms for High-Confidence Networked Medical Systems
    Designing bug-free medical device software is difficult, especially in complex on-body and implantable devices that may be used in unanticipated contexts. This project is focused on the end-to-end systems software for medical devices and includes a disposable on-body Health-Strip, adaptive RTOS design for runtime programmable control and long-term context-based data interpretation.
  • Real-Time Parallel Computing
    By 2020, embedded processors will sport 4,096 cores, server CPUs will have 512 cores and desktop chips could use 128 cores. This project’s goal is to devise a class of algorithms and complementary multi-core architectures for mission and safety-critical environments where unreliable software is not an option.
  • Networked Automotive Cyber-Physical Systems
    The automobile of the future will be networked for network-based active safety and real-time traffic congestion probing and prediction. This project’s goal is to develop wireless protocols for vehicle-to-vehicle safety, real-time traffic congestion prediction and coordinated fleet driving.