The goal of this research is to enable a broad spectrum of programmers to successfully create apps for distributed computing systems including smart and connected communities, or for systems that require tight coordination or synchronization of time. Creating an application for, say, a smart intersection necessitates gathering information from multiple sources, e.g., cameras, traffic sensors, and passing vehicles; performing distributed computation; and then triggering some action, such as a warning.

Inexpensive computation and ubiquitous embedded sensing, actuation, and communication provide tremendous opportunities for societal impact, but also great challenges in the design of networked control systems, because the traditional unity feedback loop that operates in continuous time or at a fixed sampling rate is not adequate when sensor data arrives from multiple sources, asynchronously, delayed, possibly corrupted, and — especially important for this project — the different entities that participate in the control system do not share a common clock.

Wearable electronics are widely used in health monitoring and wearable computing. The needs for comfort, biocompatibility, and operability call for special attention to new generation technologies.

The goal of this research is to gain a fundamental understanding of the integrated actuation, embedded sensing, reactive control, and distributed control needs of a cyber-physical, synthetic, distributed sensing, soft and modular tissue (sTISSUE). Realizing this cyber-physical, physiological testbed will enable surgically relevant tasks, procedures, and devices to be much more refined ahead of animal testing, which can be dramatically reduced with such high-fidelity simulators.

Verified control algorithms will be developed for the control of autonomous vehicles. Autonomous vehicles are used to perform increasingly complex tasks, safely and reliably, under changing environmental conditions. They promise to fundamentally transform our society in areas such as transportation, logistics, telecommunications, remote sensing and defense.

This project is a collaborative grant involving the University of Michigan (Award number CNS-1646392) and the University of Illinois at Urbana-Champaign (Award number CNS-1646305).

Invariant generation is crucial to the success of rigorous deductive verification tools for cyber-physical system. We develop a dedicated invariant generation toolbox for the KeYmaera X theorem prover which combines many custom invariant generation methods under a unified framework. Additionally, we develop a generalization of the method  of barrier certificates (vector barrier certificates), building on R. Bellman's work on vector Lyapunov functions.