Operating Systems Group
Operating Systems Group
Professur Betriebssysteme

Hybrid Automata

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

Spacecraft industry is developing at a rapid pace with the tendency towards distributed complex systems (swarms, constellations, formation flying, etc.) with many possible applications: planet surface observation, deep space (asteroid mining, planetary research, etc), human bases on the Moon and the Mars, etc. New space missions present new challenges due to their complexity. Non-functional system properties, with the exception for fault analysis, are not always considered to be of thorough investigation. Such as, the first unmanned space shuttle probe crashed due to unsynchronised board computers, Pathfinder rover has experienced operational problems due to the priority inversion problem, etc.

It is therefore reasonable to develop a necessary formalism and tools to support engineers in their efforts and automatise verification as far as possible, or provide necessary feedback information at the earliest during the design so that design costs are minimised.

The current research has two main objectives:

  1. To find a formal method to specify, analyse and verify non-functional system properties from the earliest design phases when information is quite scarce, and
  2. to develop a space mission meta-model with transformation rules as a formalism for composition and refinement of formal models (possibly defined using different methods) under specific conditions.
The first goal is represented by the marbles in the figure above. The growing amount of information with every new design phase is represented by the increasing circumference of the marbles. The second goal corresponds with the arrows.

The theoretical results of this work will be implemented and integrated into a software tool designed by the German Aerospace Center (Virtual Satellite).

Specially defined linear time-invariant hybrid automata (LTI-HA) are used for modelling spacecraft systems at the earliest design phases. It is possible to check space missions' feasibility by means of LTI-HA models. As a use case for non-functional system properties, timing, such as meeting deadlines and synchrony, and fault tolerance will be used. For more information see project poster

Publications

    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", Technical Report 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},

Contact