Differentielle dynamische Logiken: Automatisches Beweisen für hybride Systeme

Abstract

Die Entwicklung und Analyse komplexer physikalischer Systeme, eingebetteter Systeme und computerisierter Steuerungssysteme ist außerordentlich kompliziert, durch die steigende Verbreitung und drastische Sicherheitsrelevanz allerdings von enormer Wichtigkeit und mit hohen Kosten verbunden. Hybride Systeme sind Modelle solcher komplexen physikalischen Systeme mit sich überlagerndem diskreten Schaltverhalten und kontinuierlicher Dynamik, die durch Differentialgleichungen beschrieben wird. Als theoretisches und praktisches Fundament für die Verifikation und Analyse hybrider Systeme führen wir die differentielle dynamische Logik ein. Mit dieser kann die Korrektheit von hybriden Systemen auf natürliche und elegante Art und Weise spezifiziert und verifiziert werden, um Fehler im Systementwurf zu entdecken oder die Fehlerfreiheit nachzuweisen. Der wichtigste praktische Beitrag dieser Arbeit ist ein automatisches Beweisverfahren für die differentielle dynamische Logik, welches hybride Systeme analysiert, indem es sie sukzessiv auf Eigenschaften ihrer Bestandteile reduziert. Unser theoretisches Hauptresultat zeigt, dass dieses Verfahren hybride Systeme vollständig relativ zu elementaren Eigenschaften von Differentialgleichungen behandelt. Für komplizierte hybride Systeme stellen wir weiterhin differentielle Induktion vor, mit der Differential(un)gleichungen analysiert werden können ohne sie lösen zu müssen. Auf der Basis zahlreicher algorithmischer Fortschritte demonstrieren wir unseren Ansatz anhand erfolgreich nachgewiesener Sicherheits-, Steuerbarkeits-, Lebendigkeits- und Kollisionsfreiheitseigenschaften für Zugsteuerungen wie dem European Train Control System und Kreisverkehrmanövern im Flugverkehr.