Tipo di tesi
Tesi di laurea specialistica
Titolo
Studio ed implementazione di un algoritmo per generare i prodotti validi in Product Family Engineering
Dipartimento
SCIENZE MATEMATICHE, FISICHE E NATURALI
Corso di studi
INFORMATICA
Parole chiave
- linguaggio di programmazione Ada
- metodi formali
- model checking
- product family engineering
Data inizio appello
16/12/2011
Consultabilità
Non consultabile
Data di rilascio
16/12/2051
Riassunto (Italiano)
I temi principali di questa tesi sono la Product Family Engineering (PFE) ed il Model Checking. E' stato realizzato un ambiente che permette di:
1) descrivere il modello di una famiglia mediante una sintassi ben de finita, 2) esprimere vincoli statici e comportamentali sulle funzionalità dei prodotti, 3) generare i prodotti validi, 4) verifi care formalmente proprietà sul modello della famiglia e sui singoli prodotti. Il contributo principale e più signi ficativo è stato nel punto 3, cosa che ha dato il titolo anche a questa tesi.
Il lavoro si è focalizzato sull'attività di ricerca eseguita dal gruppo di metodi formali del CNR di Pisa nell'ambito del PFE, e sull'utilizzo di FMC, un model checker con logica branching basata su azioni (ACTL), per reti di automi defi niti come algebra dei processi in un formalismo CCS-like. Come risultato fi nale è ottenuta una applicazione accessibile mediante una semplice interfaccia web.
