Evaluierung von Suchalgorithmen zur formalen Verifikation von Raumfahrtmissionen

Dies ist die aktuellste Version dieses Eintrags.

Kurzfassung

Bei der Entwicklung von Raumfahrzeugen ändern sich in den frühen Phasen häufig das Design des Satelliten sowie die Missionsanforderungen. Jede kleine Änderung kann große Auswirkungen auf den Erfolg der Mission haben, daher muss das Satelliten-Design nach jeder Änderung erneut hinsichtlich der Missionsanforderungen verifiziert werden. Um das entwickelnde Ingenieursteam bei der Erarbeitung zweiwöchiger Machbarkeitsstudien durch eine schnelle, automatisierte Verifikation zu unterstützen, hat das Deutsche Zentrum für Luft- und Raumfahrt (DLR) ein Framework entwickelt. Dieses basiert auf einem abgewandelten Prinzip des Model Checkings, bei dem ein informierter Suchalgorithmus auf Basis eines textuell beschriebenen Modells die Verifizierung durchführt. Das Modell beschreibt das Satelliten-Design sowie die Missionsanforderungen mit Hilfe einer Verifikationssprache, die auf einer DSL basiert. Die zusätzliche Anbindung verschiedener Simulationsmodelle bietet zudem die Möglichkeit realistische Missionsszenarien nachzubilden. In dieser Arbeit sollen weitere Suchalgorithmen, unter anderem der A* Algorithmus, in das Framework integriert werden. Dazu soll eine Kostenfunktion konzipiert werden, die auch gegenläufige Zieldefinition zulässt. Dies bedeutet, dass beispielsweise nach einer minimalen Missionszeit und zeitgleich nach einer maximalen Datenmenge eines Forschungsexperiments gesucht wird. Die Eignung der Suchalgorithmen soll anhand verschiedener Evaluierungsmissionen analysiert und bewertet werden. Hierzu soll ein Satellit, angelehnt an ein echtes Raumfahrzeug, sowie gängiger Missionszenarien mit Hilfe der Verifikationssprache modelliert werden, um die Suchalgorithmen anhand praxisnaher Szenarien zu beurteilen. Zur Beschreibung des Modells sowie der Evaluierungsmissionen wird die Verifikationssprache um neue Sprachelemente erweitert.

Verfügbare Versionen dieses Eintrags

• Evaluierung von Suchalgorithmen zur formalen Verifikation von Raumfahrtmissionen. (deposited 16 Aug 2013 09:10) [Gegenwärtig angezeigt]