Logic & proofs for cyber-physical systems

@INPROCEEDINGS{DBLP:conf/cade/Platzer16,
	pdf = {pub/lpcps.pdf},
	slides = {pub/lpcps-slides.pdf},

  author    = {Andr{\'e} Platzer},
  title     = {Logic \& Proofs for Cyber-Physical Systems},
  booktitle = {IJCAR},
  longbooktitle = {Automated Reasoning, 8th International Joint Conference,
               IJCAR 2016, Coimbra, Portugal, Proceedings},
  year      = {2016},
  pages     = {15-21},
  doi       = {10.1007/978-3-319-40229-1_3},
  volume    = {9706},
  editor    = {Nicola Olivetti and
               Ashish Tiwari},
  publisher = {Springer},
  series    = {LNCS},
  keywords = {logic, cyber-physical systems, multi-dynamical systems,
               differential dynamic logic, KeYmaera X},
  abstract = {\emph{Cyber-physical systems} (CPS) combine cyber aspects
               such as communication and computer control with physical
               aspects such as movement in space, which arise frequently in
               many safety-critical application domains, including aviation,
               automotive, railway, and robotics. But how can we ensure that
               these systems are guaranteed to meet their design goals, e.g.,
               that an aircraft will not crash into another one?

               This paper highlights some of the most fascinating aspects of
               cyber-physical systems and their dynamical systems models,
               such as hybrid systems that combine discrete transitions and
               continuous evolution along differential equations. Because of
               the impact that they can have on the real world, CPSs
               deserve proof as safety evidence.

               \emph{Multi-dynamical systems} understand complex systems
               as a combination of multiple elementary dynamical aspects,
               which makes them natural mathematical models for CPS,
               since they tame their complexity by compositionality.
               The family of \emph{differential dynamic logics} achieves
               this compositionality by providing compositional logics,
               programming languages, and reasoning principles for CPS.
               Differential dynamic logics, as implemented in the theorem
               prover KeYmaera X, have been instrumental in verifying many
               applications, including the Airborne Collision Avoidance
               System ACAS X, the European Train Control System ETCS,
               automotive systems, mobile robot navigation, and a surgical
               robot system for skull-base surgery. This combination of
               strong theoretical foundations with practical theorem proving
               challenges and relevant applications makes
               \emph{Logic for CPS} an ideal area for compelling
               and rewarding research.}
}```