Modellüberprüfung für Programmiersprachen mit VeriSoft

Die Verifizierung durch Zustandsraumexploration, auch oft als "Modellüberprüfung" bezeichnet, ist eine effektive Methode zur Analyse der Korrektheit von konkurrierenden reaktiven Systemen (z.B. Kommunikationsprotokollen). Leider sind bestehende Techniken zur Modellüberprüfung auf die Verifizierung von Eigenschaften von Modellen, d.h. Abstraktionen, konkurrierender Systeme beschränkt. In diesem Papier diskutieren wir, wie die Modellüberprüfung erweitert werden kann, um direkt mit "tatsächlichen" Beschreibungen von konkurrierenden Systemen umzugehen, z.B. Implementierungen von Kommunikationsprotokollen, die in Programmiersprachen wie C oder C++ geschrieben sind. Anschließend stellen wir eine neue Suchtechnik vor, die sich für die Erkundung der Zustandsräume solcher Systeme eignet. Dieser Algorithmus wurde in VeriSoft implementiert, einem Werkzeug zur systematischen Erforschung der Zustandsräume von Systemen, die aus mehreren konkurrierenden Prozessen bestehen, die beliebigen C-Code ausführen. Als Beispiel für eine Anwendung beschreiben wir, wie VeriSoft erfolgreich einen Fehler in einem 2500-Zeilen-C-Programm entdeckte, das Roboter steuert, die in einer unberechenbaren Umgebung arbeiten.