Keynote 3 — Foundations of Programming Cyber-Physical Systems

Keynote 3 — Foundations of Programming Cyber-Physical Systems

Foundations of Programming Cyber-Physical Systems

by Rupak Majumdar, Max Planck Institute for Software Systems

CPS applications tightly integrate computation, communication, geometric reasoning, and dynamics. Despite many advances in robotics and programming languages research individually, we still lack language abstractions and reasoning principles for such systems. In this talk, I will describe work on the PGCD project, where we develop programming models and reasoning principles for multi-robot coordination. PGCD models concurrent components communicating through message passing as well as executing continuous-time motion primitives in physical space. We show how a combination of choreography types, assume-guarantee reasoning, and reactive synthesis can lead to formal verification of correctness for global specifications. We have compiled PGCD programs to ROS and show that it is feasible to verify non-trivial multi-robot coordination programs.

Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. His research interests are in formal methods and cyber-physical systems. He received “Most Influential Paper” awards from POPL and PLDI for his work in software verification. His research is funded in part by the German Science Foundations’s Collaborative Research Center on Perspicuous Systems.