Modellprüfung auf Flashspeicher-Festplatte und Grafikkarte (Model Checking on SSD and GPU)

点击翻译按钮获取中文摘要

Angesichts des weiterhin steigenden Grades an Nebenläufigkeit und der hohen Sicherheitsanforderungen an Software ist die automatische Validierung von Programmen zu einer der wichtigsten Herausforderungen der Informatik geworden. Die stetig steigende Komplexität ist nur schwer zu überblicken und macht eine automatische Fehleranalyse in Form einer Modellprüfung notwendig. Die analysierten Zustandsräume sprengen jedoch schnell die Hauptspeicherressourcen. In der externen Exploration werden deshalb besuchte Zustände (Duplikate) durch die Sortierung von Zustandsmengen auf der Festplatte eliminiert. Diese Alternative zur internen Duplikatserkennung dominiert allerdings auch den Zeitaufwand bei der Analyse. Der Einsatz von Flashspeicher ermöglicht einen schnellen Lesezugriff, um Duplikate analog zum Hauptspeicher zeitnah zu erkennen. Da der Schreibzugriff jedoch verhältnismäßig langsam ist, stellen sich algorithmische Herausforderungen an das effiziente Hashing mit Vorder- und Hintergrundspeicher. Die parallel-verarbeitende Grafikkarte kann für die effiziente Sortierung der Zustände genutzt werden. Jedoch lassen sich die Erfolge aus der GPU-basierten Sortierung von Zahlenmengen nicht unmittelbar auf die Modellprüfung übertragen. Im beantragten Projekt sollen initiale Ergebnisse der Flashspeicherund GPU-basierten Modellprüfung gefestigt und mit anderen Verfahren in der externen und parallelen Modellprüfung kombiniert werden. Die theoretische Analyse der Verfahren soll in zu erweiternden Komplexitätsmodellen geschehen.