CAREER: Logical Foundations of Cyber-Physical Systems
Lead PI:
Andre Platzer
Abstract
This project seeks to develop logical foundations for cyber-physical systems (CPS), i.e., systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPS applications abound. Ensuring their correct functioning, however, is a serious challenge. Scientists and engineers need analytic tools to understand and predict the behavior of their systems. This is the key to designing smart and reliable control. By providing such analytic foundations, this project addresses an intellectual grand challenge that has substantial scientific, economical, societal, and educational impact arising from the benefits of improved CPS analysis and design. In order to tame their complexity, this project studies CPS as multi-dynamical systems, i.e., in terms of the elementary dynamical aspects of their parts. Multi-billion dollar industries spend 50% of the development cost on control software design and testing. This cannot be sustained any longer. The foundations of computer science have revolutionized our society. We need even stronger foundations when software interacts with the physical world. Multi-dynamical systems concepts provide a unifying principle for education and enable students to focus on one dynamical aspect at a time without missing the big picture. They overcome the divide between computer science and engineering that keeps causing irreconcilable differences among design teams. This project develops cross-departmental graduate/undergraduate courses on Mathematical Foundations of CPS as prime examples of STEM integration. Long-term goals include a K-12 outreach that inspires young people to pursue science careers through an early exposure to both mathematical beauty and exciting societal challenges. CPS foundations excel in demonstrating the paramount importance of discrete and continuous mathematics, not as separate disciplines, but well-integrated.
Andre Platzer

André Platzer is a Professor of Computer Science at Carnegie Mellon University, Pittsburgh, PA, USA. He develops the Logical Foundations of Cyber-Physical Systems (NSF CAREER). In his research, André Platzer works on logic-based verification and validation techniques for various forms of cyber-physical systems, including hybrid systems, distributed hybrid systems, and stochastic hybrid systems. He developed differential dynamic logic and differential invariants and leads the development of the CPS verification tool KeYmaera X.

André Platzer received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, and was named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009 and one of the AI's 10 to Watch 2010 by the IEEE Intelligent Systems Magazine.

Performance Period: 02/01/2011 - 01/31/2018
Institution: Carnegie-Mellon University
Sponsor: National Science Foundation
Award Number: 1054246