|
Thesis on Software Engineering and Formal Methods
|
| The SRA division of ITC-irst and the DIT department of the University of Trento do research in the fields of Software Engineering and Formal Methods (DIT, ITC-irst). One of the activities in this areas of research consists in the integration of Formal Methods and Software Engineering developing a Software Development Process where Formal Verification is light-weightly integrated. Within this idea of integration there are several theses avialble for students interested. Further informations can be retrieved by getting in touch with Marco Pistore or with Marco Roveri. |
| 1. | Animation of Requirements Specifications | |
| Scope: | Software Engineering and Formal Methods | |
| Background: |
Requirements specification is one of the most critical phases in the software development process.
This is the phase where the software engineer captures and analyzes the desires and the intentions of
the stake-holder, and performs on them goals-oriented analysis that eventually lead to the requirements
of the system-to-be. Incompleteness and misunderstandings in this phase of the development process
can have dramatic impact on the final product.
In this framework, particularly effective for the interaction with the stake-holder is the possibility of animating the formal specification of the requirements. With animation is meant the ability of generating and exploring interactively the behaviors of the system-to-be that are compatible with the requirements specifications, and the possibility to show these behaviors in a graphical notation easily understandable to the stake-holders. |
|
| Goal: | The goal of the thesis is to design and develop an interactive graphical animator for requirements specification within Formal Tropos. | |
| Relevant links: |
|
|
| Skills: | Knowledge of the Linux operating system, knowledge of the C programming language, knowledge of graphical scripting languages. | |
| Contacts: | Marco Pistore, Marco Roveri | |
| 2. | Verification of Requirements Specifications | |
| Scope: | Software Engineering and Formal Methods | |
| Background: |
Requirements specification is one of the most critical phases in the software development process.
This is the phase where the software engineer captures and analyzes the desires and the intentions of
the stake-holder, and performs on them goals-oriented analysis that eventually lead to the requirements
of the system-to-be. Incompleteness and misunderstandings in this early phase of the development process
can have dramatic impact on the final product.
In this framework, it is of particular interest the ability to exhaustively verify wether the specification satisfy some desired properties, e.g., in a car insurance domain, it is never the case that two insurance companies pay twice for the same damage, or that, in a e-commerce application verify wether a credit card is charged if and only if the order is registered. In order to perform this kind verification suing a reasonable amount of resources (e.g. time and memory) it is necessary to concentrate on an abstract version of the model, where the "relevants" elements of the specification for the property being verified are taken into account. Theoretical results guarantee that if the property is proven to hold in the abstract model, then it holds in the original model too. |
|
| Goal: | The goal of the thesis is to design and develop techniques able to identify a subset of the specification on top of which run the verification. This work is part of the Formal Tropos project that aims to the integration of formal methodology inside Tropos. | |
| Relevant links: |
|
|
| Skills: | Knowledge of the Linux operating system, knowledge of the C programming language, knowledge of propositional logics. | |
| Contacts: | Marco Pistore, Marco Roveri | |