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 (FDIR) for satellites and space exploration systems; system-level diagnosability, diagnosis and root-cause analysis; anomaly detection and FDIR based on machine learning techniques. Topics to be investigated include techniques for contract-based design and contract-based safety assessment, 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, the use of machine learning techniques for anomaly detection and fault classification and their integration with FDIR.

The developed techniques will be implemented and evaluated using tools for system-software engineering such as the COMPASS and the TASTE tools. This study is aligned with the topics investigated in various industrial projects carried out at FBK, such as the COMPASTA and AIFDIR projects, funded by the European and Italian Space Agencies.

This PhD opportunity is a collaboration between Fondazione Bruno Kessler and the University of Trento – Space Science and Technology. For more information on this call and how to apply, please visit the website of the University of Trento (https://www.unitn.it/it/dottorati/dottorato-di-interesse-nazionale-space-science-and-technology-sst).