| Property Assurance | ||
| Scope: | Model Checking/Requirements Engineering/Formal Methods | |
| Background: | Fill here | |
| Goal: |
Development of advanced "property assurance" techniques. Here the focus is on the inspection/improvement of the quality of a set of LTL/PSL requirements; the aim is to provide the designer with a deep knowledge of the requirements he wrote, and strong confidence about the fact that they really capture what the intended design must exhibit. Classical Model Checking techniques can be applied to the analysis of set of requirements, however, they do not fit well larger sets for which reduction techniques can be exploited instead. Proper techniques must be singled out from the literature, possibly tailored to our need, or possibly defined from scratch. For instance, abstraction techniques based on "Cone of influence" reduction can be experimented to value their effectiveness in solving the problem. These techniques will be integrated within the "Property Assurance Tool" that is part of the PROSYD project due deliverables. |
|
| Relevant links: | ||
| Skills: | Knowledge of the Linux operating system, knowledge of the C programming language, knowledge of propositional logics and automata theory. | |
| Contacts: | Marco Roveri, Alessandro Cimatti, Simone Semprini, | |