Model-checking software product lines with FTS

Model-checking software product lines with FTS

Prof. Patrick Heymans
University of Namur, Belgium

DEI - Sala Conferenze
10 Novembre 2011
Ore: 10.00


Software Product Line (SPL) engineering is a software engineering paradigm that exploits the commonality between similar software products to reduce their cost and time-to-market. Many SPLs are critical and would benefit from efficient verification through model checking. SPL model checking is more difficult than for single systems because the number of product variants is potentially huge (exponential in the number of features of the SPL). To address this problem, we introduced Featured Transition Systems (FTS), a formal and compact representation of SPL behaviour. We also defined efficient algorithms to model check FTS against properties expressed in temporal logic, and implemented several prototypes. Early experiments suggest that FTS are a promising approach towards efficient verification of SPLs in practice. Our current work includes applying simulation relations and compositional reasoning to further improve performance. We also want to extend our theory to address real-time and probabilistic SPLs.

Ghezzi Carlo
Molzam Sharifloo Amir

Area di ricerca:
Metodologie e architetture software avanzate