Algoritmi efficienti per model checking parametrico di modelli markoviani discreti

I cambiamenti imprevedibili affliggono continuamente i sistemi software e possono causare gravi conseguenze, compromettendo in modo irrimediabile la qualità del servizio, paralizzando il sistema, causando in certi casi la violazione dei requisiti del software stesso. Questi cambiamenti possono coinvolgere componenti critici del sistema, profili operazionali e requisiti arrivando talvolta agli ambienti di sviluppo. L'adozione di modelli software e tecniche di Model Checking a run-time, potrebbe essere utile per supportare sistemi automatici di reasoning nella valutazione di questi cambiamenti: la rilevazione di configurazioni dannose permetterebbe così di reagire, attivando appropriate contromisure automatiche. Le tecniche di MC tradizionali e i tools a loro associati non sono adatti, per come sono progettatti attualmente, ad essere utilizzati a run-time, poiché non sono in grado di soddisfare i vincoli rigidi imposti dall'esecuzione on-the-fly (al volo) in termini di memoria e tempo di esecuzione. In questo elaborato verranno proposti metodi formali di Model Checking per valutare vincoli di affidabilità su sistemi modelizzabili come Catene di Markov a Tempo Discreto Parametriche (PMC). E' stato sviluppato un software basato sul calcolo algebrico matriciale che, dato un vincolo di affidabilità ed un modello del sistema, restituisce un insieme di espressioni che possono essere utilizzate per una efficiente verifica dei requisiti a run-time. Verrà inoltre effettuato un confronto dell'approccio qui proposto con i Model Checker probabilistici esistenti mostrando come ognuno di questi sia utilizzabile nel campo della verifica a run-time.