|Thesis abstract: |
In the last few years, automatic processing of information and data pervades every aspect of the modern enterprises. The criticality of the applications and processes that modern software processes have to manage is constantly increasing. In this context, software failure can be costly. Thus, it is crucial to guarantee that the software satisfies of a set of predefined properties, which represent the functional and non-functional requirements that the system must fulfill. Software verification and in particular Model Checking aims to assure in a formal, rigorous, mathematical way, that certain functional and non functional properties hold in the system under development.
We wish to support a stepwise development of models and separate verification of the refinement steps. Although there have been a surprising improvements that led to the development of efficient model checkers, the available mainstream techniques are not directly applicable to incomplete and evolving specifications in which some parts may change over time. In particular, most existing model-checking approaches require a complete re-check of the system against its requirement every time that a part of the software is changed (or re-designed). If changes are frequent, formal verification becomes a bottleneck of the development process.
To solve this problem, model-checking should be equipped with techniques taking into account both reusability and incrementality. Reusability is a matter of designing verification algorithms able to generate and use previously generated information, in a way to minimize the effort in the current and future verifications. In particular, when a change occurs, the verification algorithm does not verify the whole system from scratch, but uses the information (e.g., constraints that the sub-component must satisfy) previously generated to reduce the verification effort. Incrementality concerns the possibility of verifying the system through a sequence of consecutive incremental steps, as the different parts of the software are designed and developed. It would thus be useful to be able to check if incomplete specifications meet the specified requirements.
This research mainly aims to develop algorithms, methodologies and approaches to reduce the verification effort in an agile context, where the software is subject to frequently changes. We will consider different aspects related to this problem, starting from modeling formalisms (e.g., LTS and Statechart) and property logics (e.g. CTL, LTL) to the verification algorithm itself, considering both functional and non functional properties.