When: Tuesday, April 29, 10:00 a.m.- 11:30 a.m.

Where: 3305 Newell-Simon Hall

André Platzer, University of Oldenburg

SCS Faculty Candidate Talk

Abstract:
Hybrid systems model complex physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce Differential Dynamic Logic as a logic with which correctness properties of hybrid systems with parameterized system dynamics can be specified and verified naturally. As a verification technique, we introduce a proof calculus that is suitable for automation and works compositionally, i.e., it reduces properties of hybrid systems to properties of their parts. Systematically, we derive a verification procedure from the calculus and present an iterative background closure procedure to tackle the complexities of integrating decision procedures for real arithmetic. For handling systems with complicated continuous dynamics, we further present a continuous generalization of induction. Finally, we develop a fixed point algorithm for computing the differential invariants required for continuous induction, and we introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. As a systematic combination of logic-based techniques, we obtain a sound verification procedure that is particularly suitable for parametric hybrid systems. We demonstrate our approach by verifying safety, controllability, liveness, and collision avoidance properties in case studies ranging from train control over car platooning to air traffic management, including collision avoidance in aircraft roundabout maneuvers.

<< Back