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.

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.

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.

Abstract: In many important situations, analytically predicting the behavior of physical systems is not possible. For example, the three dimensional nature of physical systems makes it provably impossible to express closed-form analytical solutions for even the simplest systems. This has made experimentation the primary modality for designing new cyber-physical systems (CPS).

Abstract: Cyber-physical systems (CPS) encompass the next generation of computerized control for countless aspects of the physical world and interactions thereof. The typical engineering process for CPS reuses existing designs, models, components, and software from one version to the next.