FTS4VMC: uno strumento per disambiguazione e family-based model checking degli FTS

A Featured Transition System (FTS) is a formal behavioural model for software product lines, which represents the behaviour of all the products of an SPL in a single compact structure associating transitions with features that condition their existence in products. An FTS may contain unreachable transitions in any products (called dead transitions), mandatory transitions if their source state is reachable (called false optional transitions) and states from which only certain products can progress (called hidden deadlocks). This internship report shows how we built the FTS4VMC tool that enables users to detect the previously described ambiguities, to remove them from the FTS and to verify properties using family-based model checking on live FTS (i.e, without hidden deadlock).

Un Featured Transition System (FTS) è un modello comportamentale formale per le linee di prodotti software (SPL), che rappresentano il comportamento di tutti i prodotti di una SPL in un unica struttura compatta che associa transizioni con feature che determinano la loro presenza nei prodotti. Un FTS può contenere transizioni irraggiungibili da ogni prodotto (chiamate dead transition), transizioni obbligatorie se il loro stato sorgente è raggiungibile (dette false optional transition) e stati dai quali solo certi prodotti possono procedere (detti hidden deadlock). Questo rapporto di stage mostra come abbiamo costruito lo strumento FTS4VMC che consente agli utenti di individuare le ambiguità precedentemente descritte, di rimuoverle dagli FTS e di verificare proprietà utilizzando controlli family-based su FTS senza stati di hidden deadlock.