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

Scheda Progetto di ricerca

Condividi sui principali social network: Facebook    Delicious    add to Connotea    add to CiteUlike
Data inizio
14 ottobre 2010

Durata (mesi) 
24

Dipartimenti
Informatica

Responsabili (o referenti locali)
Pravadelli Graziano

Descrizione

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 V sono legate ad attività di formazione per le imprese coinvolte in VERILAB in base al seguente programma:

Modulo 1: Modellazione delle specifiche (80 ore)
- le logiche temporali e il linguaggio PSL (property specification language);
- la modellazione di SW embedded tramite macchine a stati finiti estese;
- i linguaggi per la descrizione di sistemi embedded HW/SW, con particolare attenzione al linguaggio SystemC TLM 2.0.

Modulo 2: La verifica del SW embedded (80 ore)
- la verifica funzionale;
- introduzione alle tecniche di verifica formale;
- model checking e verifica basata su asserzioni;
- mutation analysis e mutation testing;
- tecniche automatiche per la generazione di sequenze di test.

Modulo 3: Applicazione in contesto produttivo (30 ore)
- utilizzo dell’ambiente di verifica sviluppato in un contesto reale;
analisi e interpretazione dei risultati ottenuti durante la fase di verifica in contesto reale.

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
STMProducts
Finanziamento: assegnato e gestito dal dipartimento
Programma: ART66 - Attività Commerciale

Partecipanti al progetto

Giuseppe Di Guglielmo
Incaricato alla ricerca
Luigi Di Guglielmo
Incaricato alla ricerca
Franco Fummi
Professore ordinario
Graziano Pravadelli
Professore associato
Stefano Soffia
Aree di ricerca coinvolte dal progetto
Sistemi ciberfisici
Computer systems organization - Embedded and cyber-physical systems
ornamento
Inizio pagina