Verifica formale di Software modellato e generato automaticamente (Verilab - Azione I)

Data inizio
14 ottobre 2010
Durata (mesi) 
24
Dipartimenti
Informatica, Ingegneria per la medicina di innovazione
Responsabili (o referenti locali)
Pravadelli Graziano

Il presente progetto, finanziato dal Raggruppamento Temporaneo di Impresa denominato VERILAB, si colloca nell'ambito delle attività del progetto VAFER approvato dalla Regione Veneto il cui obiettivo consiste nella realizzazione di uno strumento di verifica semi-formale per applicazioni embedded basato su assertion-based verification.
Il progetto è diviso in 3 azioni (Azione I, Azione III e Azione V).
Le attività che il dipartimento di informatica svolgerà nell'ambito dell'azione I sono:
-analisi dello stato dell’arte relativo alla assertion-based verification per SW embedded;
-scrittura di proprietà PSL per i casi di studio selezionati durante il progetto VAFER;
-integrazione di checker nel flusso di assertion-based verification dinamica;
-integrazione di strumenti di model checking nel flusso di assertion-based verification formale;
-generazione automatica di sequenze di test sfruttando mutation analysis e mutation testing

Enti finanziatori:

EDALab s.r.l.
Finanziamento: assegnato e gestito dal Dipartimento
Programma: ART66 - Attività Commerciale
MCE Meccanica s.r.l.
Finanziamento: assegnato e gestito dal Dipartimento
Programma: ART66 - Attività Commerciale
STM Products s.r.l.
Finanziamento: assegnato e gestito dal Dipartimento
Programma: ART66 - Attività Commerciale

Partecipanti al progetto

Graziano Pravadelli
Professore ordinario
Stefano Soffia
Aree di ricerca coinvolte dal progetto
Sistemi ciberfisici
Embedded and cyber-physical systems

Attività

Strutture

Condividi