Cyber-Physical Programming

Objectives

The goal of this course unit is to thoroughly prepare the student to a disciplined way of developing and analysing cyber-physical systems; this requires going over their basic principles, adequate models of computation, and respective tools. At the end of the course the student will,

  1. be proficient in standard models of cyber-physical computation, namely (extensions of) hybrid automata and hybrid programming languages;
  2. understand the differences between the various notions of equivalence for these two models;
  3. be able to recognise and properly treat Zeno behaviour;
  4. be proficient in the tools Uppaal and Lince, which cover both model checking and testing/simulation of cyber-physical systems;
  5. understand in which ways the state-of-the-art is limited, and the potential outcomes of solving these limitations;
  6. be able to properly coordinate the previous learning outcomes in order to design and reason about complex cyber-physical systems.

Program

  1. Hybrid automata (and respective extensions) as models for cyber-physical computation; notions of simulation and bisimulation.
  2. The use of hybrid automata to address specific aspects of cyber-physical computation.
  3. The tool Uppaal; Case studies.
  4. Cyber-physical programming: algorithmic principles and compositionality.
  5. Operational and denotational semantics for cyber-physical computation.
  6. The tool Lince; Case studies.

Bibliography

  • The theory of hybrid automata. T. A. Henzinger. Published in the Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), 1996.
  • Verification and control of hybrid systems. Paulo Tabuada. Published by Springer, 2009; ISBN: 978-1-4419-0223-8.
  • Logical foundations of cyber-physical systems. AndreĢ Platzer. Published by Springer, 2018; ISBN: 978-3-319-63587-3. - The formal semantics of programming languages. Glynn Winskel. Published by MIT Press, 1993. ISBN: 978-0-262-23169-5.
  • An adequate while-language for hybrid computation. Sergey Goncharov and Renato Neves. Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages (PPDP), 2019

Updated: