Model-checking software product lines with FTS

Model-checking software product lines with FTS

Prof. Patrick Heymans
University of Namur, Belgium

DEI - Sala Conferenze
November 10th, 2011
at 10.00 a.m.


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

Research area:
Advanced software architectures and methodologies