Modellazione e verifica di sistemi embedded ibridi per piattaforme multiprocessore (PRIN 2007)

Data inizio
22 settembre 2008
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Fummi Franco

La modellazione e la verifica di piattaforme embedded multiprocessore sono problematiche strettamente legate che vengono ancora gestite con metodologie e
linguaggi non correlati. Inoltre, le tradizionali tecniche di modellazione a livello RT, che fino a qualche anno fa permettevano di gestire agevolmente la progettazione di sistemi digitali, non sono più adatte per le moderne piattaforme embedded. Infatti, la complessità di tali piattaforme, costituite da una rete di parti HW e SW interagenti, sta crescendo molto velocemente, in modo particolare per i sistemi ibridi, in cui sono coinvolti sia componenti continue che discrete.
In tale contesto, appare pertanto evidente che le attuali metodologie di sviluppo soffrono, da un lato la mancanza di continuità tra i livelli di astrazione, e dall'altro lo scarso riutilizzo delle strategie di verifica tra i livelli stessi. L'introduzione della modellazione a livello transazionale (TLM), della verifica basata su asserzioni (ABV) e di linguaggi di descrizione a livello di sistema quali, ad esempio, SystemC e SystemVerilog, mira al superamento di tali problemi e permette una maggior omogeneità tra modellazione e verifica a tutti i livelli di astrazione fino al livello RT compreso. Tuttavia, la specifica iniziale di un sistema embedded ibrido necessità di un formalismo ad hoc per la gestione delle componenti continue e discrete del sistema, che è difficile da ottenere usando linguaggi come SystemC o SystemVerilog.
In tale ambito, l'utilizzo degli automi ibridi garantisce un'implementazione semplice ed efficiente della doppia natura (discreta e continua) di un sistema ibrido.
Pertanto, l'obiettivo di questa unità di ricerca consiste nello sviluppo di una metodologia e di un insieme di prototipi per la modellazione e verifica di sistemi
embedded ibridi per piattaforme multiprocessore che sfrutti sia la teoria degli automi ibridi, che le tecniche di modellazione e verifica basate su TLM e ABV. La
metodologia proposta si svilupperà, quindi, in quattro attività strettamente correlate:
1. modellazione e verifica di automi ibridi a partire da specifiche definite tramite proprietà formali;
2. estrazione di vincoli funzionali e temporali da automi ibridi per la generazione semi-automatica di modelli SystemC TLM;
3. raffinamento e verifica dei modelli SystemC tramite asserzioni e generazione automatica di sequenze di test (necessarie per la verifica dinamica delle asserzioni);
4. applicazione dei modelli SystemC ottenuti dopo i passi precedenti e configurazione della piattaforma multiprocessore di riferimento.
La strategie di modellazione e verifica proposte saranno implementate in quattro prototipi: ARIADNE per la modellazione e verifica di automi ibridi, SEXTRACT per
la generazione semi-automatica di modelli SystemC TLM, MILEDI per il raffinamento dei modelli SystemC lungo tutti i livelli TLM, e MultiCover per la verifica
post-raffinamento.

Enti finanziatori:

PRIN VALUTATO POSITIVAMENTE
Finanziamento: richiesto
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Nicola Bombieri
Ricercatore
Franco Fummi
Professore ordinario
Graziano Pravadelli
Professore associato
Aree di ricerca coinvolte dal progetto
Sistemi ciberfisici
Computer systems organization - Embedded and cyber-physical systems

Attività

Strutture