hybrid systems


Visible to the public Sound Invariant Generation for Continuous and Hybrid Systems

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.


Visible to the public Multi-Resolution Model and Context Aware Information Networking for Cooperative Vehicle Efficiency and Safety Systems

Large scale deployment of connected and automated vehicles is impeded by significant technical and scientific gaps, especially when it comes to achieving real-time and high accuracy situational awareness for cooperating vehicles. This CAREER project aims at closing these gaps through developing fundamental information networking methodologies for coordinated control of automated systems. These methodologies are based on the innovative concept of modeled knowledge propagation. The approach is to utilize the novel concepts of model communication and its derived multi-resolution networking.


Visible to the public Belief-Aware Cyber-Physical Systems

During the development process of CPS, an analysis of whether the system operates safely in its target environment is of utmost importance. For many applications of CPS research such as the transportation industry, this implies interconnected research in formal verification of CPS with research on knowledge representation and reasoning in multi-agent systems. The need for such research has become tragically clear in transportation accidents, one notorious case being the Air France 447 flight incident.