logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-11272011-210504


Tipo di tesi
Tesi di laurea specialistica
Autore
SULOVA, ALDI
URN
etd-11272011-210504
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
Relatori
relatore Prof.ssa Gnesi, Stefania
relatore Dott. Mazzanti, Franco
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
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 definita, 2) esprimere vincoli statici e comportamentali sulle funzionalità dei prodotti, 3) generare i prodotti validi, 4) verificare formalmente proprietà sul modello della famiglia e sui singoli prodotti. Il contributo principale e più significativo è 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 definiti come algebra dei processi in un formalismo CCS-like. Come risultato finale è ottenuta una applicazione accessibile mediante una semplice interfaccia web.
File