Dr. Stefan Mitsch (Computer Science Department, Carnegie Mellon University, US) is going to lecture on
“Real Proofs for Real Cyber-Physical Systems – Theorem Proving and Verified Runtime Monitoring”
at
https://authgr.zoom.us/j/8353677440?pwd=ZGVtYjk5L0Fkbk9mQll6bjgrdTFqQT09
Meeting ID: 835 367 7440
Passcode: 843065
on Monday March 28th, 2021, at 16:30. The lecture is organised by the Postgraduate Program on Technologies of Interactive Systems of the School of Informatics and is open to the academic community of Aristotle University.
Abstract:
Formal verification plays a crucial role in making cyber-physical systems safe with strong guarantees about the system under a certain model of the system’s behavior and interaction with its environment. In CPS, runtime safety is challenging because it requires predictions about physical dynamics in order to act ahead of time, before physics makes violating the desired safety properties inevitable. Building formal predictive hybrid systems models that include both computations and physical behavior, however, becomes increasingly difficult due to (semi-)autonomy through poorly understood learning components in increasingly unconstrained operating environments. This poses the double challenge of validating formal models from observations while simultaneously providing safety guarantees about unverified learned components and the observed runtime behavior. This talk discusses techniques for hybrid systems theorem proving and for hybrid systems runtime monitoring to distinguish between the system
operating inside or outside the model boundaries. Together, these techniques provide true runtime safety guarantees by transferring proofs about models to proofs about the CPS runtime behavior.
Short bio:
Stefan Mitsch is a research faculty member of the Computer Science Department at Carnegie Mellon University. His research focuses on modeling, formal verification, and verified runtime monitoring methods and tools for cyber-physical systems, with logic as their unifying centerpiece. He is particularly interested in applying formal methods to (semi-)autonomous transportation systems (e.g., aircraft and drones, self-driving cars and ground robots, railroad protocols) with learning components.
