Il progetto EFFORT mira allo sviluppo di una metodologia, supportata da prototipi, per migliorare la progettazione e la verifica di applicazioni embedded per piattaforme configurabili. La metodologia si baserà sul modello delle macchine a stati finiti estese (EFSM) e utilizzerà SystemC come linguaggio di riferimento per la modellazione sia del SW che delle periferiche HW incluse nella piattaforma selezionata.
In primo luogo, verrà sviluppato un prototipo per generare in modo automatico modelli SystemC di EFSM che descrivono l’applicazione embedded. Tali EFSM saranno estratte automaticamente da modelli UML, e verranno verificate usando tecniche semi-formali basate su verifica di proprietà (property checking) e generazione automatica di sequenze di test (automatic test pattern generation). Quindi, i componenti HW, inclusi nella piattaforma, verranno modellati in SystemC e simulati assieme al modello SystemC dell’applicazione SW, tramite il riuso di sequenze di test e di proprietà, per verificare la funzionalità dell’intero sistema.
Infine, a partire dal modello SystemC dell’applicazione SW, verrà generato in modo semi-automatico il corrispondente codice C che sarà successivamente verificato tramite l’uso di un simulatore architetturale temporalmente accurato.
L’efficacia della metodologia verrà provata modellando e verificando un’applicazione embedded fornita da STM Products.
L’obiettivo principale del progetto consiste nel definire un ambiente di progettazione e validazione per applicazioni embedded. In tale contesto, il progetto intende affrontare sia aspetti legati alla ricerca scientifica che aspetti inerenti l’implementazione tecnologica. Gli obiettivi dal punto di vista della ricerca scientifica sono:
- introduzione del modello EFSM per la modellazione e verifica di SW embedded;
- introduzione di vincoli e modelli formali, nell’ambito della progettazione di SW embedded basata su EFSM, per la formalizzazione e verifica delle specifiche tramite la definizione di proprietà formali;
- definizione di metodologie per la verifica funzionale di SW embedded sfruttando le caratteristiche del linguaggio SystemC a livello TLM (transactional level modelling);
- definizione di metodologie per la verifica temporalmente accurata di modelli misti HW/SW.
Gli obiettivi dal punto di vista dell’implementazione tecnologica sono:
- implementazione di un software per estrarre modelli EFSM dalla descrizione UML del SW embedded e generare automaticamente il codice C/SystemC corrispondente;
- implementazione di strumenti per la verifica di modelli EFSM rispetto alle specifiche;
- implementazione di un simulatore per la simulazione funzionale di applicazioni embedded e la generazione automatica di sequenze di test ottimizzate;
- implementazione di un modello di simulazione basato su SystemC per le periferiche HW incluse nella piattaforma di riferimento;
- integrazione del simulatore funzionale con un simulatore architetturale (HSN), che modella anche gli aspetti temporali, per l’esecuzione e la verifica del codice binario dell’applicazione embedded;
- esecuzione delle sequenze di test sull’ambiente di simulazione HW/SW per confrontare l’efficacia dell’utilizzo di strategie di verifica basate sulla misura della copertura dei difetti con i tradizionali processi per il controllo di qualità.