Programmanalysen zur Verbesserung der Softwaremodellprüfung

Abstract

Die Softwarequalität kann mittels Modellprüfung gesteigert werden, indem formale Eigenschaften von Software bzw. davon abgeleitete Modelle verifiziert werden. Die derzeit verfügbaren Modellprüfer sind nicht in der Lage, Quelltexte komplexer Softwareprojekte selbständig, automatisiert und ohne Fehlalarme zu überprüfen. Um Fehlalarme zu reduzieren, wurden präzise Modelle in Form von symbolischen Kellersystemen (SPDS) betrachtet und Verfahren entwickelt, welche die Softwaremodellprüfung verbessern. Da Modellprüfer sehr sensitiv auf die Größe des betrachteten Zustandsraumes reagieren, wurden vorrangig Techniken zu seiner Verkleinerung entworfen, ohne den Wahrheitsgehalt der zu prüfenden Eigenschaften zu verändern. Neben neuen theoretischen Erkenntnissen wurde experimentell gezeigt, dass so in einigen Fällen die Modellprüfung erst ermöglicht wird und in anderen Fällen sich die Modellprüfung sogar ganz erübrigt.