2018

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.

Advances in the effective integration of networked information systems, sensing and communication devices, data sources, decision making, and physical infrastructure are transforming society, allowing cities and communities to surmount deeply interlocking physical, social, behavioral, economic, and infrastructural challenges. These novel sociotechnical approaches enable increased understanding of how to intelligently and effectively design, adapt, and manage Smart and Connected Communities (S&CC).

The goal of this project is to demonstrate that new cyber-physical architectures will enable closed-loop sensor networks to be shared among multiple applications and to dynamically allocate sensing and computing resources necessary to analyze sensor data and perform sensor actuation.