Space systems have reached an unprecedented degree of complexity. The design process has to guarantee not only the functional correctness of the implemented system, but also its dependability and resilience with respect to run-time faults. Hence, the design process must characterize the likelihood of faults, mitigate possible failures, and assess the effectiveness of the adopted mitigation measures.

Formal methods have been increasingly used over the last decades to deal with the shortcomings of designing complex systems, in different domains. Formal methods are based on the adoption of a formal, mathematical model of the system, shared between all actors involved in the system design, and on a tool-supported methodology to aid all the steps of the design, from the definition of the architecture down to the final implementation in HW and SW.

The objective of this study is to advance the state-of-the-art in space system design using formal methods. In particular, it will investigate new techniques for model-based system and software engineering, to support the design, mission preparation and operations of space systems. The potential research directions include fault detection, isolation, and recovery for satellites; system level diagnosis and diagnosability based on telemetry; digital twins for satellites. Topics to be investigated include techniques for contract-based design and contract-based safety assessment, advanced verification techniques based on compositional reasoning, the analysis of the timing aspects of fault propagation, the characterization of transient and sporadic faults, the analysis of the effectiveness of fault mitigation measures in presence of complex fault patterns, and the modeling and analysis of systems with continuous and hybrid dynamics.

The developed techniques will be implemented and evaluated using tools for system-software engineering such as the COMPASS tool and the COMPASTA tool, based on the TASTE tool chain.