Ph.D XL

Supervisor: Alessandro Cimatti, co-sup: Stefano Tonetta

Room: FBK

Mail: fantinato.filippo@spes.uniud.it

Research Project

Requirements validation and diagnosis of contract based designed complex systems

Nowadays, we are surrounded by systems which involve several critical aspects, where a fault can result in the loss of a lot of money, or worse the death of many people, like trains, cars, satellites and space rovers.

Systems like those described above are called critical systems and, to make it more complicated, technology goes fast and all systems are becoming more and more complex, performing an increasing number of critical functions.
This calls for effective and rigorous methods to find defects early in the development process, to guarantee safety and correctness, and to reduce the costs of certification.

Among the techniques that can be exploited, contract based design is a very promising paradigm for building correct-by-construction systems, leading to a very efficient way to structure complex systems.
Another crucial part for developing correct software is requirements analysis. Such requirements bring to those properties that must hold in the final system and this requires strong validation techniques based on formal methods.

Nevertheless, in requirements validation there is no system to be analyzed and the requirements themselves are the entity under analysis.

This leads to proper logics to represent them in the different contexts and a way to figure out whether all these properties are realizable or not. If a set of requirements is not realizable, it is useful to have a way to provide diagnostic information about the unrealizable properties, like the explanation of the unrealizability and the minimal unrealizable set of formulas.

My PhD project regards the above topics, that is requirements validation and diagnosis of complex systems built exploiting the contract based design paradigm.

The objectives of the proposed research are to enchant and develop new requirements validation and diagnosis methods for contract based design systems.