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

Profile Card Research project

Share this record with your favourite social network: Facebook    Delicious    add to Connotea    add to CiteUlike
Starting date
October 14, 2010

Duration (months)
24

Departments
Computer Science

Person in charge
Pravadelli Graziano

Description

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

Sponsors:

EDALab s.r.l.
Funds: assigned and managed by the department
Syllabus: ART66 - Attività Commerciale
MCE Meccanica s.r.l.
Funds: assigned and managed by the department
Syllabus: ART66 - Attività Commerciale
STMProducts
Funds: assigned and managed by the department
Syllabus: ART66 - Attività Commerciale

Project participants

Giuseppe Di Guglielmo
Incaricato alla ricerca
Luigi Di Guglielmo
Incaricato alla ricerca
Franco Fummi
Full Professor
Graziano Pravadelli
Associate Professor
Stefano Soffia
Research areas involved in the project
Sistemi ciberfisici
Computer systems organization - Embedded and cyber-physical systems
ornamento
Top