Formal verification of parametric timed automata with TABEC

In the context of formal verification of systems, particularly digital systems, Model Checking (MC) stands out as one of the most effective automated techniques. Considering a formal model of the system under analysis and a specific formal property, MC aims to verify the validity of this property within the given system. One of the most relevant formalisms in MC is represented by Timed Automata (TAs), which can act as acceptors of languages, the nature of which depends on the adopted definition of TAs. A significantly relevant problem associated with TAs concerns determining the emptiness of their language, known as the emptiness problem. It is known that, for conventional TAs, this problem is generally decidable, allowing for the creation of a decision algorithm. The problem becomes generally undecidable when the definition of TAs allows parameters. This thesis focuses on examining the emptiness problem for a specific category of TAs known as parametric non-resetting test TAs (nrtTAs). For a particular subclass of this model, the emptiness problem proves to be decidable. This led to the creation of a decision algorithm, which was implemented inside a specifically developed tool. Furthermore, the tool's capacity of randomly generating TAs has allowed its enrichment with random testing functionalities, including the incorporation of oracle prediction capabilities. This implies the tool's ability to anticipate the outcomes of tests before their execution. The validity of both theoretical and practical obtained results was ultimately confirmed through a comprehensive testing phase, encompassing the correctness of algorithmic responses, the scalability of the tool, and the accuracy of provided oracle predictions.

Nel contesto della verifica formale dei sistemi, specialmente dei sistemi digitali, il Model Checking (MC) rappresenta una delle tecniche automatiche più efficaci. Considerando un modello formale del sistema in analisi e una specifica proprietà formale, il MC si prefigge di verificare la validità di tale proprietà all'interno del sistema in questione. Uno dei formalismi più rilevanti nel MC è rappresentato dagli Automi Temporizzati, altresì noti come Timed Automata (TA), i quali possono assumere la funzione di accettori di linguaggi, la natura di questi ultimi dipendente dalla definizione adottata di TA. Un problema di notevole rilevanza associato ai TA riguarda la determinazione della vacuità del loro linguaggio, conosciuto come il problema della emptiness. È noto che per TA convenzionali, tale problema risulta essere generalmente decidibile, permettendo di conseguenza la creazione di un algoritmo decisionale risolutivo. La questione assume un carattere generale di indecidibilità qualora la definizione dei TA contempli la presenza di parametri. La presente tesi si dedica all'analisi del problema della emptiness per una specifica categoria di TA nota come non-resetting test TA (nrtTA) parametrici. Per una sottoclasse particolare di tale modello, il problema della emptiness risulta essere decidibile. Questo ha comportato la creazione di un algoritmo decisionale di cui è stata effettuata l'implementazione attraverso uno strumento appositamente sviluppato. Inoltre, la generazione randomica di TA da parte dello strumento ha consentito l'arricchimento del medesimo con funzionalità di testing randomico, incluso l'inserimento di abilità di predizione da oracolo. Tale circostanza implica la capacità dello strumento di anticipare l'esito dei test prima che questi vengano eseguiti. La validità dei risultati teorici e pratici ottenuti è stata infine confermata mediante un'esaustiva fase di testing, sia per quanto concerne la correttezza delle risposte fornite dall'algoritmo, sia per quanto riguarda la scalabilità dello strumento, sia per quanto concerne la correttezza delle previsioni da oracolo fornite.