Conventional digital computers are not the only devices that need to be programmed. This tutorial studies the programming language principles of cyber-physical systems (CPS), which are those that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPSs have many important applications, e.g., in robotics, aerospace, and automotive domains, but require careful designs to meet stringent safety demands and have many surprises in store for the uninitiated.

In order to do justice to the rich behaviors of a CPS, their mathematical programming models need to handle multi-dynamical systems, including, at least, the discrete dynamics of stepwise controller computations and the continuous dynamics of their differential equations. This tutorial explains how differential dynamic logic (dL) can be used to recover from those radical changes to the very essence of computation. We will show how to use dL and its implementation in the KeYmaera X theorem prover to design, specify, and verify the safety of CPS programs in an instructive chain of examples. More detail about the presented approach can also be found in the recent textbook on Logical Foundations of Cyber-Physical Systems.

André Platzer is an Associate Professor of Computer Science at Carnegie Mellon University. He develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to answer the question how we can trust a computer to control physical processes.

André Platzer has a Ph.D. from the University of Oldenburg, Germany, received an ACM Doctoral Dissertation Honorable Mention and NSF CAREER Award, and was named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI’s 10 to Watch by the IEEE Intelligent Systems Magazine.