HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Simulation-Based Abstractions for Software Product-Line Model Checking

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087659
Contributor : Uli Fahrenberg Connect in order to contact the contributor
Submitted on : Wednesday, November 26, 2014 - 2:39:05 PM
Last modification on : Friday, February 4, 2022 - 3:15:08 AM
Long-term archiving on: : Friday, February 27, 2015 - 12:20:25 PM

File

icse12.pdf
Files produced by the author(s)

Identifiers

Citation

Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, et al.. Simulation-Based Abstractions for Software Product-Line Model Checking. ICSE 2012 : 34th International Conference on Software Engineering, Jun 2012, Zürich, Switzerland. pp.672 - 682, ⟨10.1109/ICSE.2012.6227150⟩. ⟨hal-01087659⟩

Share

Metrics

Record views

579

Files downloads

415