FTS4VMC: disambiguazione e family-based model checking sugli FTS

The following report describes FTS4VMC, a tool which allows to analyze a featured transition system (FTS), which models the behavior of all products of a software product line (SPL); discover and remove the ambiguities from it; verify an ACTL formula against it with the VMC model checker; render it using Graphviz; translate it in the Promela language for further work with the SPIN model checker. The already mentioned ambiguities can be of three types: dead transitions, i.e. transitions which are not reachable in any product; false optional transitions, i.e. transitions modelled as optional in the FTS which results in mandatory ones in each product; hidden deadlock states, i.e. states from which a transition can be executed only in some products.

La presente relazione descrive FTS4VMC, un tool che consente di: analizzare un featured transition system (FTS), il quale modella il comportamento dei prodotti di una software product line (SPL); individuarne e rimuoverne le ambiguità; verificare proprietà su di esso tramite il model checker VMC; visualizzarlo tramite Graphviz; tradurlo nel linguaggio Promela. Le ambiguità menzionate possono essere di tre tipi: dead transitions, ovvero transizioni irraggiungibili in ogni prodotto; false optional transitions, ovvero transizioni modellate come opzionali nell' FTS ma che risultano obbligatorie in ogni prodotto; hidden deadlock states, ovvero stati le cui transizioni uscenti possono essere eseguite solo in alcuni prodotti.