Logical Analysis of Hybrid Systems
Abstract:
Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They 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 talk describes how logic and formal verification can be lifted to hybrid systems. It presents the theoretical and practical foundations of logical analysis of hybrid systems. The talk describes a logic for hybrid systems called differential dynamic logic and surveys a perfectly compositional proof technique. This approach is implemented in the verification tool KeYmaera and has been used used successfully for verifying nontrivial properties of aircraft, railway, car, robotics, and robotic surgery applications. The logical approach also shows how verification techniques for continuous dynamics can be lifted to hybrid systems by a complete axiomatization.