Interpretazione astratta e model checking per la verifica di sistemi embedded

Data inizio
21 febbraio 2003
Durata (mesi) 
46
Dipartimenti
Informatica
Responsabili (o referenti locali)
Giacobazzi Roberto
Parole chiave
Interpretazione astratta, Model checking, Verifica

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à

Enti finanziatori:

Ministero dell'Istruzione dell'Università e della Ricerca
Finanziamento: assegnato e gestito da un ente esterno all'ateneo
Programma: FIRB

Partecipanti al progetto

Samir Genaim
Roberto Giacobazzi
Professore ordinario
Isabella Mastroeni
Professore associato
Roberto Segala
Professore ordinario
Nicola Fausto Spoto
Professore associato
Damiano Zanardini

Attività

Strutture