Professur Betriebssysteme
Professur Betriebssysteme
Professur Betriebssysteme

Hybride Automaten

Multi-phase model-based spacecraft design process with growing amount of information and transformation rules for transitions between the phases

Komplexe verteilte Systeme (wie Swarms, Konstellationen, Formationsflüge usw.) werden immer öfter in der Raumfahrtindustrie entwickelt. Die Anwendungen dafür sind sehr unterschiedlich, von Überwachung der Planetenoberfläche und interplanetaren Forschung bis zu bemannten Raumflüge. Neue Raumfahrtmissionen stellen wegen ihrer Komplexität große Herausforderungen dar. Jedoch werden die nichtfunktionale Eigenschaten, mit der Ausnahme von Fehleranalyse, ziemlich oft übersehen. Als ein Beispiel kann man die fehlende Synchronisation von Boardrechner am Testflug von (noch) unbemannten Spaceshuttles nennen, was zum Versagen der gesamten Mission führte.

Es ist daher sinnvoll, einen Formalismus zu entwickeln, der die Ingineuere von Raumfahrtsystemen unterstützt und entlastet, indem bestimmte Verifikationsschritte für nichtfunktionale Eigenschaften automatisiert werden.

Zwei wesentlichen Ziele dieser Forschung sind:

  1. Suche nach einer formalen Methode zur Spezifikation, Analyse und Verifikation von nichtfunktionalen Eigenschaften von den frühesten Designphasen, und
  2. Entwicklung eines Raumfahrt Meta-Metamodells mit Transformationsregeln, die die Komposition und Verfeinerung von formalen Modelle (auch unter unterschiedlichen Modellierungsmethoden definierte) unterstützt.
Das erste Ziel wird in dem oben stehenden Bild in Form von Kugeln mit dem wachsenden Radius dargestellt, da die Information, die über das zu entwickelnde System oder ihr Umgebung zur Verfügung steht, mit Zeit wächst. Das zweite Ziel ist durch die grünen Pfeile dargestellt, die die Transformationsregeln festlegen.

Die gewonnenen theoretischen Erkentnisse werden dann implementiert und in ein von dem Deutschen Zentrum für Luft- und Raumfahrt entwickelten Tool (Virtueller Satellit) integriert.

Für die Modellierung von Raumfahrtsystemen in den frühesten Designphasen werden besonders für diesen Zweck definierte lineare Zeit-invariante hybride Automaten (LTI-HA) verwenden. Im Moment ist es möglich, mit diesem Formalismus ein System grob zu modellieren, um die Machbarkeitsanalyse durchzuführen. Besonders interessant in der Zukunft werden die nichtfunktionale Eigenschaften wie Timing, e.g. Deadlineseinhaltung oder Synchronität, und Fehlertoleranz. Für mehr Informationen sehen Sie Projekt-Poster (auf Englisch)

Veröffentlichungen

    2017

  1. Jafar Akhundov, Michael Reißner, Matthias Werner, "Using Hybrid Automata for Early Spacecraft Design Evaluation", in Proceedings of the 26th International Workshop on Concurrency, Specification and Programming, 2017 
    @inproceedings{akhundov_using_2017,
    address = {Warsaw, Poland},
    title = {Using {Hybrid} {Automata} for {Early} {Spacecraft} {Design} {Evaluation}},
    booktitle = {Proceedings of the 26th {International} {Workshop} on {Concurrency}, {Specification} and {Programming}},
    author = {Jafar Akhundov and Michael Reißner and Matthias Werner},
    month = sep,
    year = {2017},
    keywords = {composition, haautomata}


    2. 2016

  2. Jafar Akhundov, Peter Tröger, Matthias Werner, "Considering Superposition in the Composable Hybrid Automata", in Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, 125-140, 2016 
    @INPROCEEDINGS{Akh:HAComposition:2016,
    author = {Jafar Akhundov and Peter Tröger and Matthias Werner},
    TITLE = {Considering Superposition in the Composable Hybrid Automata },
    booktitle = {Proceedings of the 25th International Workshop on Concurrency, Specification and Programming},
    YEAR = 2016,
    month = 9,
    pages = {125--140},
    address = {Rostock, Germany},
    keywords = {composition haautomata},
    url = {http://ceur-ws.org/Vol-1698/}
  3. Jafar Akhundov, Matthias Werner, Volker Schaus, Andreas Gerndt, "Using Timed Automata to Check Space Mission Feasibility in the Early Design Phases", in IEEE Aerospace, 2016 
    @conference {Akh:aeroconf2016:TA,
    title = {Using Timed Automata to Check Space Mission Feasibility in the Early Design Phases},
    booktitle = {IEEE Aerospace},
    year = {2016},
    month = {03/2016},
    publisher = {IEEE},
    organization = {IEEE},
    address = {Big Sky, MT},
    keywords = {haautomata},
    author = {Jafar Akhundov and Matthias Werner and Volker Schaus and Andreas Gerndt}


    4. 2013

  4. Jafar Akhundov, "Implementation of the Global Physical Time for the Domain Model of The Virtual Path of the DLR Hand-Arm System", Forschungsbericht 5,, 2013 
    @TechReport{Akh:Globtime:2013,
    author = {Jafar Akhundov},
    title = {Implementation of the Global Physical Time for the Domain Model of The Virtual Path of the DLR Hand-Arm System},
    type = {DLR-IB 572-2013/24},
    year = 2013,
    number = {5},
    organization = {German Aerospace Center (DLR), Institute for Robotics and Mechatronics},
    address = {DLR Oberpfaffenhofen},
    month = 6,
    pages = 103,
    keywords = {haautomata},
    url = {http://elib.dlr.de/87115},

Ansprechpartner