Simulation-based abstractions for software product-line model checking

Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre Yves Schobbens, Patrick Heymans, Axel Legay

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

54 Citations (Scopus)

Abstract

Software Product Line (SPL) engineering is a software engineering paradigm that exploits the commonality between similar software products to reduce life cycle costs and time-to-market. Many SPLs are critical and would benefit from efficient verification through model checking. Model checking SPLs is more difficult than for single systems, since the number of different products is potentially huge. In previous work, we introduced Featured Transition Systems (FTS), a formal, compact representation of SPL behaviour, and provided efficient algorithms to verify FTS. Yet, we still face the state explosion problem, like any model checking-based verification. Model abstraction is the most relevant answer to state explosion. In this paper, we define a novel simulation relation for FTS and provide an algorithm to compute it. We extend well-known simulation preservation properties to FTS and thus lay the theoretical foundations for abstraction-based model checking of SPLs. We evaluate our approach by comparing the cost of FTS-based simulation and abstraction with respect to product-by-product methods. Our results show that FTS are a solid foundation for simulation-based model checking of SPL.
Original languageEnglish
Title of host publicationProceedings - International Conference on Software Engineering
Number of pages11
PublisherIEEE
Publication date1 Jan 2012
Pages672-682
ISBN (Print)978-1-4673-1066-6
ISBN (Electronic)978-1-4673-1065-9
DOIs
Publication statusPublished - 1 Jan 2012
Event34th International Conference on Software Engineering - Zürich, Switzerland
Duration: 2 Jun 20129 Jun 2012
Conference number: 34

Conference

Conference34th International Conference on Software Engineering
Number34
Country/TerritorySwitzerland
CityZürich
Period02/06/201209/06/2012
SeriesProceedings of the International Conference on Software Engineering
ISSN0270-5257

Fingerprint

Dive into the research topics of 'Simulation-based abstractions for software product-line model checking'. Together they form a unique fingerprint.

Cite this