Temporale Verifikation mit Transitionsinvarianten

Abstract

Temporale Verifikation von Programmen befasst sich mit der Erstellung von Korrektheitsaussagen über Programmausführungen. Dabei besteht die Hauptherausforderung in der Synthese von geeigneten Hilfsaussagen, welche die Gültigkeit einer temporalen Eigenschaft implizieren. Es existieren bereits Verifikationswerkzeuge, die Sicherheitseigenschaften, d.h. die Abwesenheit von unerwünschten Ereignissen, automatisch nachweisen können. Diese Werkzeuge verwenden Abstraktion, um die Programmkomplexität zu bewältigen. Für Lebendigkeitseigenschaften, die das Auftreten von erwünschten Ereignissen garantieren, gab es bislang kein automatisches Ve- rifikationswerkzeug, da die notwendigen Hilfsaussagen (Ranking-Funktionen) schwer zu berechnen sind und die klassische Abstraktion für die Lebendigkeitseigenschaften nicht anwendbar ist. Transitionsinvarianten stellen eine neue Art von Hilfsaussagen für die Verifikation von Lebendigkeitseigenschaften dar. Sie sind einfacher zu finden als Ranking-Funktionen und können mit Abstraktion kombiniert werden. Dadurch schaffen Transitionsinvarianten eine Grundlage für die Konstruktion von automatischen Werkzeugen, die ihre Praxistauglichkeit erfolgreich nachwies.