[DL] PhD Position on Requirements Validation in Trento - 19 Sept. Deadline for Application

[Marco Bozzano]

    >>> Apologies for multiple postings <<<

A PhD position in the area of

"Formal Methods for Requirements Validation of Resilient Systems"

is available in the Embedded Systems Research Unit (ES) at Bruno
Kessler Foundation (FBK), Center for Information Technology. FBK is a
private research institution based in Trento (Italy) and operating in
different scientific fields and disciplines. The PhD program is
carried out in collaboration with the University of Genova. The place
of study is Trento, Italy.

===============================================
  Deadline for application: 19 September 2017
===============================================

For information about how to apply, please visit:
https://www.studenti.unige.it/postlaurea/dottorati/graduatoriexxxiiiciclo/reopsecuita/
https://www.studenti.unige.it/postlaurea/dottorati/graduatoriexxxiiiciclo/reopsecueng/

For more information about FBK and the ES research unit, please visit:
https://www.fbk.eu/
http://es.fbk.eu/

For more information about Trento and the FBK PhD program, please visit:
http://phd.fbk.eu/

=============
  PhD topic
=============

Title:
Formal Methods for Requirements Validation of Resilient Systems

Research areas:
Formal Methods, Requirements Engineering, Safety and Security,
Temporal Logic, Formal Verification, Model Checking

Description:
In the last decade, an increasing number of applications needs
software systems that are open and interconnected and, at the same
time, require a high level of assurance of critical mission, safety,
or security requirements. New formal methods must be developed to
ensure the system resilience to internal and external factors.
The study will focus on the formalization and validation of
requirements for resilient systems. The objective is to investigate
new formal languages that are able to capture the resilience of
systems to internal faults or external attacks and new methods to
analyze these properties solving problems such as satisfiability,
realizability, and diagnosability. The study will build on existing
model checking techniques for transition systems with first-order
constraints and temporal properties and on the results of past and
current projects such as EURAILCHECK and CITADEL.

Link to the group or personal webpages:
http://es.fbk.eu
https://es.fbk.eu/projects/eurailcheck
http://citadel-project.eu