Categorical Interpretation of Inter-Model Consistency with Respect to Non-Functional System Properties in the Multiphase Space Mission Planning and Design
With the complexity of the modern space systems steadily growing, both in a monolithic spacecraft or distributed swarms, the correctness-by-design becomes an important approach for the mission planing process. In this talk I will introduce the general idea of my research and then give more details about one of its subtopics.
The goal of the research is to implement a domain-specific language designed for the purpose of specifying an evolving complex space system (cyber-physical system) in the multi-phase design process and integrate it into the Virtual Satellite project implemented at the German Aerospace Center (DLR). Furthermore, special verification tools and methods are to be analyzed, created and implemented for model checking the given system description against design and mission constraints, which are also part of the specification. For this purpose, a meta-model must be created which will then be translated into the DSL syntax and will allow to describe a space system of high complexity and be reusable and expandable at each of the phases of the design. The constraints of interest will be the non-functional system properties , such as Synchrony, Mobility (Real-Space-Time constraints) and Complexity/Emergence.
In the following talk/paper, I will introduce the first steps done in creating such a meta-model by analyzing the critical properties of a space mission which form a basis for the design and define its transformations and extensions in the terms of category theory. This will become the formal foundation and the skeleton of the future work, which will then build upon it. This model will be created by analyzing several existing space missions, both already successful or still in the planning phase, so that their general properties could be defined. Each stage discards some of the information of the previous phase or previous best practices and uses some of them to generate new information. This forms a morphism between the specification sheets and reports, which will be the objects of the category of a general space mission. The information flow inside each design stage can also be modeled by a category and will be analyzed separately for each design step.