Model checking lots of systems: efficient verification of temporal properties in software product lines
Abstract
In product line engineering, systems are developed in families and differences between family members are expressed in terms of features. Formal modelling and verification is an important issue in this context as more and more critical systems are developed this way. Since the number of systems in a family can be exponential in the number of features, two major challenges are the scalable modelling and the efficient verification of system behaviour. Currently, the few attempts to address them fail to recognise the importance of features as a unit of difference, or do not offer means for automated verification.
BibTeX
@inproceedings{Classen-al:ICSE10,
author = {Andreas Classen and
Patrick Heymans and
Pierre{-}Yves Schobbens and
Axel Legay and
Jean{-}Fran{\c{c}}ois Raskin},
title = {Model checking lots of systems: efficient verification of temporal properties in software product lines},
booktitle = {ICSE (Part I)},
pages = {335--344},
publisher = {{ACM}},
year = {2010},
}