Metodi formali e strumenti per la verifica di sistemi critici

The thesis shows the results achieved in the use of formal methods to anlayze some case studies coming from the industrial environment. The focus of the thesis is on the development of control systems and on the benefits of a formal approach in this field. The aim of the thesis is twofold: i) describing the methodology applied during the analysis of the case studies ii) presenting a software tool to assist the users in the application of the proposed methodology. During the analysis of the case studies, the work did not focus just on the verification phase of a system but even the goodness of requirements has been considered. An exhaustive technique to evaluate if a given set of requirements is complete has been developed. The proposed methodology and the developed tool have been both used to analyze some case studies provided by AgustaWestland.

Questa tesi documenta i risultati ottenuti durante l’applicazione di metodi formali ad alcuni esempi tratti da reali casi industriali, mostrando l'efficacia del supporto che tali metodi possono fornire durante la realizzazione di software nell’ambito dei sistemi di controllo. Lo scopo della tesi è sia la descrizione della metodologia applicata sia la presentazione di uno strumento software che renda tale metodologia di semplice applicazione. L'analisi effettuata non si è focalizzata solamente sulla parte di verifica del sistema ma anche sulla parte di scrittura dei requisiti, definendo una tecnica per valutarne la loro esaustività. La metodologia e lo strumento software sono stati entrambi utilizzati per l'analisi di alcuni casi industriali forniti dall'AgustaWestland.