Formal Methods for Automated Reasoning and Reliability Analysis of Autonomous Space Systems

Università degli Studi di Trento

Space Science and Technology
Cycle: 42

This research focuses on the application of formal methods and automated reasoning to ensure the reliability and safety of autonomous space systems. As satellite platforms transition toward higher levels of autonomy, there is a critical need for rigorous analysis techniques that can handle complex system behaviors. The research will investigate integrated frameworks for automated safety and reliability assessment, enabling the formal validation of system-level properties. Specifically, the project will leverage contract-based design to manage architectural complexity, automated generation of safety artifacts (such as Fault Trees and FMEA), and formal verification of FDIR strategies. Furthermore, the research will explore the use of formal monitors and safety cages to provide dependability guarantees for components using AI. By building on state-of-the-art tools like OCRA and xSAP, the goal is to develop a robust MBSE flow that supports the design and certification of next-generation autonomous missions.

This position is reserved for candidates of Kenyan nationality.

FBK Contact

Are you ready to join FBK international community?

We welcome motivated applicants who are passionate about research, eager to learn, and driven by curiosity to explore new ideas.

Six reasons to become a PhD student at FBK

At FBK, our PhD program is designed to develop highly specialized researchers in a unique, stimulating environment

RESEARCH
AT FBK​

A Hub of innovation and collaboration​

TOWARD PHD EXCELLENCE

FBK stands out as one of Italy’s leading research institutions

international
network

National and international
companies and universities

learning opportunities

Explore a world of learning
at FBK

Discover Trento

One of the most Italy’s
livable city

Join FBK

A truly international
community