Un approccio per la specifica e la verifica di requisiti fuzzy

The diffusion of adaptive systems that change at runtime depending on the conditions under which they operate and the consequent need for constant monitoring of the level of satisfaction of requirements make the traditional crisp analysis inadequate. Hence, it's important to represent the level of satisfaction of a requirement violations and distinguish serious from those small or temporary. This thesis proposes a fuzzy temporal framework for verifying properties via a modified version of model checking that introduces uncertainty in the time domain. The model of the system under analysis is based on automata and on such a model the degree of satisfiability of the system requirements are measured. In particular the tecnique evaluates the degree to which the system requirements are met. The thesis is structured as follows. Initially, the preliminary concepts necessary for the definition of the proposed framework and the state of the art with regard to fuzzy logic, fuzzy temporal logic, fuzzy automata, probabilistic automata and timed automata are shown. Then he temporal fuzzy framework FuLTL is presented. The syntax and semantics of the language, together with some examples of formulas, are described. After introducing the language, the model used for describing the system under analysis and the technique for verifying properties inspired by the model checking are formally defined. In particular the formalism of timed automata with discrete fuzzy functions is described. These automata are a discrete version of timed automata, which model the system based on changes in the degree of truth of atomic fuzzy propositions which represent the parameters to evaluate. The method of verification and evaluation of the formulas FuLTL is shown and a case study that summarizes the whole approach is reported. Finally, the data structures, the implementation of the various algorithms proposed, the FuLTLParser, some experiments on the evaluation of FuLTL formulas and some tests for the evaluation of efficiency are presented.

La diffusione di sistemi adattativi che si modificano a runtime a seconda delle condizioni in cui operano e la conseguente necessità di un costante monitoraggio del livello di soddifazione dei requisiti fanno sì che non sia più sufficiente la tradizionale valutazione crisp. E' fondamentale, quindi, poter rappresentare il livello di soddisfazione di un requisito e distinguere violazioni piccole o temporanee da quelle gravi. Oggetto di questa tesi è l'introduzione di un framework temporale fuzzy per la verifica formale, che permetta di esprimere incertezza nel dominio temporale. Il sistema in analisi viene modellizzato con una particolare tipologia di automi arricchiti con timer e variabili fuzzy, basati sul paradigma ECA (Evento-Condizione-Azione). Su tale modello si valuta con che grado vengono soddisfatti i requisiti del sistema. Il lavoro è strutturato come segue. Inizialmente vengono introdotte le nozioni preliminari necessarie per la definizione del framework proposto e lo stato dell'arte sugli argomenti correlati con questo lavoro, quindi la logica fuzzy, la logica temporale fuzzy, gli automi fuzzy, gli automi probabilistici e gli automi temporizzati. In seguito, viene presentato FuLTL, il framework temporale fuzzy. Vengono illustrate la sintassi e la semantica del linguaggio corredate da alcuni esempi di formule. Una volta introdotto il linguaggio, viene definito formalmente il modello usato per la specifica del sistema in analisi e la tecnica per la verifica di proprietà ispirata al model checking. In particolare, viene introdotto il formalismo degli automi temporizzati discreti con funzioni fuzzy, una versione discreta degli automi temporizzati, che descrivono il sistema in base alle variazioni del grado di verità di proposizioni fuzzy atomiche che rappresentato i parametri da valutare. Questi automi costituiscono il modello sul quale vengono valutate le formule FuLTL. E' inoltre presentata una metodologia di verifica e di valutazione delle formule FuLTL. L'intero approccio viene descritto anche attraverso un caso di studio. Infine, vengono presentate le strutture dati, l'implementazione dei diversi algoritmi proposti, il parser per il linguaggio FuLTL, gli esperimenti per la verifica della correttezza della valutazione di formule FuLTL e gli esperimenti per la valutazione dell'efficienza dell'applicazione.