Two PhD positions available in collaboration with the University of Trento on formal-methods-related topics

Twp PhD positions are available at FBK, in collaboration with the University of Trento. The deadline for application is May 15th.

Symbolic Model Checking techniques for embedded systems (1 grant)

Abstract: Techniques based on formal methods for the verification and validation of embedded and safety-critical systems are becoming increasingly important, due to the growing complexity and importance of such systems in every aspect of modern society. Despite the major progress seen in the last twenty years, however, the application of formal methods remains a challenge in practice, due to factors such as poor scalability, lack of automation, the interplay between computation and physical aspects, or the increasing complexity of the software and its configurations.

This project will investigate novel techniques for the application of formal methods to the design, verification, and validation of embedded systems, with particular emphasis on safety-critical application domains such as railways, automotive, avionics, and aerospace. A particular attention will be devoted to improving the scalability and degree of automation of formal methods techniques, with a specific focus on symbolic model checking methods using satisfiability and satisfiability modulo theories solvers as symbolic reasoning engines. Importantly, in addition to researching novel theoretical results, a significant part of the project activities will be devoted to the implementation of the techniques in state-of-the-art verification tools developed at FBK and their application to real-world problems in collaboration with our industrial partners.

Contact: Alberto Griggio

Failure Propagation Analysis for Safety Assessment of Complex Systems (1 grant)

Abstract: The design process of complex systems must guarantee not only the functional correctness of the implemented system, but also its safety, dependability, and resilience with respect to run-time faults. To this aim, complex systems implement mechanisms to timely detect components' faults and to isolate them, before they can propagate and cause system failures. Hence, the design process must characterize the likelihood and severity of faults, identify the set of possible hazards and failure conditions, mitigate possible consequences, and assess the effectiveness of the adopted mitigation measures.

Model-Based Safety Analysis (MBSA) is listed as an acceptable and recommended means of compliance to perform safety assessment in the latest issue of SAE ARP4761A, specifically for analyzing failure propagation. MBSA is based on the adoption of a formal, mathematical model of the system and on a tool-supported methodology to assist the generation of safety artifacts. State-of-the-art tools for MBSA implement functionalities to generate Minimal Cut Sets (MCS) from a fault propagation model and a Top-Level Event (TLE); perform automated fault injection into a behavioral design model to generate the corresponding safety model; generate Minimal Cut Sets from a fully behavioral dynamical model and a TLE; perform various kind of validation of fault propagation models against behavioral models.

The objective of this study is to advance the state-of-the-art in failure propagation analysis and safety assessment of complex systems. In particular, it will investigate extensions of existing formalisms to deal with aspects such as the timing of fault propagation, the characterization of transient and sporadic faults, and the analysis of the effectiveness of fault mitigation measures in presence of complex fault patterns. Moreover, this study will investigate the use of fault propagation models for the design of fault detection, isolation and recovery (FDIR) components. To this aim, fault propagation models will be extended with observability information and used to solve problems such as anomaly detection, diagnosis, root-cause analysis, and prognosis. Finally, this study will aim to bridge the gap between fault propagation models and fully behavioral system models used for the design and safety assessment of complex systems.

Contact: Marco Bozzano

Call for Application

Application Page