• linguaggio di programmazione Ada
• metodi formali
• model checking
• product family engineering

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.