PhD Grant on Model-based system-software engineering and formal methods for space systems
Jun 17, 2025
A new PhD position is opened, in collaboration with the University of Trento (PhD program on Space Science and Technology - SST), on the topic of Model-based system-software engineering and formal methods for space systems.
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.
For more information, see the web page with the Details about funded positions.
To apply, visit the Ph.D. programmes page of the University of Trento.
The deadline for application is July 16th at 4pm.
Application Page
-
PhD Grant on Model-based system-software engineering and formal methods for space systems
-
PhD positions in collaboration with the University of Trento on formal-methods-related topics
-
VAIPOSA Kick Off Meeting
-
New Software Developer Position in the Field of Formal Methods
-
Distinguished artifact award at TACAS conference