Verifikation Nebenläufiger Programme

Abstract

Unsere Gesellschaft vertraut maßgeblich und stetig zunehmend auf verteilte IT Systeme. Allerdings sind Entwurf und Verifikation nebenläufiger Programme berüchtigt komplizierte, zeitintensive und fehleranfällige Aufgaben, selbst für Fachexperten. Der Grund dafür ist die enorme (un- endliche) Menge an verzahnten Ausführungen nebenläufiger Programme. All diese Ausführungen müssen in einem formalen Korrektheitsbeweis erfasst und berücksichtigt werden. Solche Beweise basieren bekanntermaßen auf induktiven Invarianten über den globalen Programmzustand. Die Erarbeitung induktiver Invarianten für konkrete Implementierungen ist zwar theoretisch möglich, aber praktisch undenkbar. In dieser Dissertation präsentieren wir eine Verifikationsmethodik basierend auf dem Konzept der schrittweisen Verfeinerung, welche die Konstruktion formaler Korrektheitsbeweise grundlegend vereinfacht. Wir präsentieren eine Programmiersprache zur kompakten Beschreibung von Beweisen über mehrere Abstraktionsebenen. Eine mächtige Beweisregel unterteilt das Verifikationsproblem in zahlreiche automatisierbare Unterprobleme. Neue Beweistaktiken für asynchrone Programme ermöglichen die Reduktion von komplexen nebenläufigen Ausführungen zu simplen sequenziellen Ausführungen. Unsere Methodik ist in unserem statischen Analyseprogramm CIVL implementiert und dessen Effektivität wird in zahlreichen Fallstudien demonstriert. CIVL wurde bereits in mehreren Publikationen anderer Forscher verwendet.