Document - Static analysis and family-based model checking of featured transition systems with VMC

2021

Conference article Open Access

Static analysis and family-based model checking of featured transition systems with VMC

Ter Beek M. H., Mazzanti F., Damiani F., Paolini L., Scarso G., Valfrè M., Lienhardt M.

SPL Variability FTS MTS Static analysis Formal verification VMC

A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.

Source: SPLC'21 - 25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021

Publisher: ACM Press, New York, USA

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:456541,
	title = {Static analysis and family-based model checking of featured transition systems with VMC},
	author = {Ter Beek M. H. and Mazzanti F. and Damiani F. and Paolini L. and Scarso G. and Valfrè M. and Lienhardt M.},
	publisher = {ACM Press, New York, USA},
	doi = {10.1145/3461002.3473071},
	booktitle = {SPLC'21 - 25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021},
	year = {2021}
}