it gb
it gb

J. Sproston - Verifica automatica di sistemi probabilistici

È ampiamente riconosciuto che i problemi rilevati all'inizio del processo di sviluppo di un sistema sono meno costosi da correggere rispetto a quelli rilevati in seguito. Le tecniche di modellazione e verifica formale possono essere utilizzate per rilevare errori o inefficienze nella fase di progettazione, consentendoci di verificare e comprendere a fondo la progettazione di un sistema prima della sua costruzione. Il model checking è un metodo di verifica automatico per determinare se il modello di un sistema soddisfa una certa specifica ed è stato applicato in un'ampia varietà di contesti, inclusi sistemi safety-critical, robotica e systems biology.

Per molti sistemi è importante rappresentare fedelmente aspetti che riguardano la probabilità di eventi (ad esempio, guasti, perdita dei pacchetti, comportamento di esseri viventi, condizioni meteorologiche, ecc.). Ciò ha portato al model checking probabilistico, in cui la probabilità del comportamento del sistema è modellata esplicitamente usando formalismi come le catene di Markov. Utilizzando metodi di model checking probabilistico, potremmo essere in grado di determinare, ad esempio, che possono verificarsi errori di sistema con una probabilità sufficientemente bassa. In questa presentazione verrà presentata un'introduzione sintetica al model checking probabilistico.


Relatore: Jeremy Sproston

E-mail: Ci1D39uBmIK2wQFW0cTO]#[4Ws1v1hzww21pCyOobAG