Il progetto si occupera' di studiare e sviluppare modelli teorici per la verifica di sistemi embedded, in particolare sistemi software ibridi e real-time, combinando le tecniche di interpretazione astratta e model checking.
Il progetto ha il duplice scopo di definire nuovi strumenti automatici di verifica basati su model checking e interpretazione astratta, e di sviluppare una tassonomia di linguaggi modali di specifica e modelli di sistema in relazione alla precisione ed al costo computazionale della procedura di verifica.
Le attivita' previste nella unita' di Verona sono organizzate nel modo seguente:
- Task 1: Completezza di modelli astratti
In questo task siamo principalmente interessati nel progetto sistematico di logiche temporali complete per un dato sistema, anche approssimato o astratto, e nella pallicazione del model checking completo nell'analisi del flusso di informazione sicura in componenti software di sistemi embedded, e.g. programmi Java byte-code. Il primo aspetto e' essenziale al fine di sviluppare una tassonomia di logiche temporali in base alla struttura del sistemi da verificare ed alla completezza. Il secondo aspetto invece e' particolarmente importante per verificare automaticamente il flusso di informazione in Java byte-code.
- Task 2: Interpretazione astratta per il model checking di sistemi real-time e ibridi.
In questo ambito siamo interessati nella estensione della teoria sviluppata per progettare interpretazioni astratte complete all'approssimazione di model checking di sistemi con componenti continue (real-time o ibridi e probabilistici). Questo puo' essere ottenuto innanzitutto generalizzando le operazioni per il raffinamento di domini astratti all'astrazione di sistemi ibridi a componenti continue (e.g. con equazioni differenziali negli stati). In questa direzione intendiamo considerare come base di partenza recenti studi sulla domain-theory per sistemi probabilistici e real-time, ed alcuni lavori recenti su interpretazione astratta di programmi con probabilità
