Considering Concurrency in Early Spacecraft Design Studies.
Jafar Akhundov, Peter Tröger, Matthias Werner · CS&P · 2015
In real-world spacecraft systems, concurrent system activities must be constrained for energy efficiency and functional reasons. Such constraints must be considered in the early design phases, in order to avoid costly reiterations and modifications of the proposed system design in later phases. Although some initial attempts for using formal specifications exist in the domain, there is a lack of concurrency support in the utilized approaches. In this paper, we therefore first formalize an existing domain-specific language for specifying spacecraft designs and their constraints. Since this language does not support the modelling of concurrency issues, we extend it accordingly and map it to standard timed automata, based on a general system model. The new-style specifications can now be processed with existing and proven automata modelling tools, which enables faster and more reliable feasibility checks for early spacecraft system designs.