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.

Recently there is an increasing availability of smart wearables including smart watches, bands, buttons and pendants. Many of these devices are part of human-in-the-loop Cyber Physical Systems (CPS). With future fundamental advances in the intersection of communications, control, and computation for these energy and resource limited devices, there is a great potential to revolutionize many CPS applications.