Record #519268

DFG project G:(GEPRIS)115655855

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

Coordinator	Professor Dr. Stefan Edelkamp
Grant period	2009 - 2018
Funding body	Deutsche Forschungsgemeinschaft
	DFG
Identifier	G:(GEPRIS)115655855

Note: 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.

Recent Publications

There are no publications

Record created 2023-02-02, last modified 2024-09-27

Similar records

Rate this document:

(Not yet reviewed)

Add to personal basket
Export as Author List with IDs BibTeX (UTF-8), EndNote XML, EndNote Text, RIS, MARC, Print MARC, MARCXML, DC,
Request correction
Submit fulltext

guest :: login PUBDB
		Search		Submit		Personalize Your alerts Your baskets Your searches		Help