Assuring the Safety, Security and Reliability of Medical Device Cyber Physical Systems (NSF CPS) - Project page

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.

High-Confidence Medical Device Software and Systems (NSF) - Project page

The development and production of medical device software 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 and effective. There are three projects that we are pursuing: development of the reference implementation and assurance cases of Generic Patient Controlled Analgesia (GPCA), model-based development of the Pacemaker Challenge, design of Generic Decision Support Architecture (G-CDSA). The latter is based on our experience in building a smart alarm for post CABG surgery patients, a decision caddy for vasospasm risk analysis, models of blood glucose control guidelines and a closed-loop PCA controller.

Real-Time Embedded Systems: Compositional Scheduling Framework (NSF, ARO) - Project page

Real-time systems are ones in which correctness depends not only on logical correctness but also on timeliness. In the real-time systems community, substantial research efforts have concentrated on the schedulability analysis problem, which determines whether timing requirements imposed on the system can be satisfied. However, there is no widely accepted technique that supports the compositionality of timing requirements, i.e., how component-level timing requirements can be independently analyzed, abstracted, and composed into the system-level timing requirements. We have developed a compositional real-time scheduling framework for supporting the compositionality of timing requirements. Our compositional scheduling framework is supported by the CARTS tool.

Quantitative Trust Management (ONR MURI) - Project page

In modern computing, distributed topologies are becoming more prevalent as designers take advantage of the bandwidth, file diversity, and scalability such systems offer. Frequently, nodes have the ability to both request and provide services from other users. This is inherently risky; decentralized models lack the notions of authenticity, reliability, and accountability that monolithic servers can provide. Nonetheless, well-behaved decentralized systems are advantageous. Behavior recognition and enforcement are the role of trust and reputation systems. The design and study of these programs is the primary focus of the Quantitative Trust Management Multiple University Research Initiative (QTM-MURI).

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.

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.