Paper in volume 14 of STTT (Int J Softw Tools Technol Transfer)
The first comprehensive paper on SNIP has been published in volume 14 number 5 of the International Journal on Software Tools for Technology Transfer (STTT). The paper was published online in June already, but the issue finally appeared last week.
The paper, titled Model checking software product lines with SNIP, is basically an extract of my PhD thesis (Chapter 9), describing SNIP’s input language (fPromela), its FTS interpretation, the command-line usage of SNIP and the implementation details of the FTS algorithms. Here is the abstract:
We present SNIP, an efficient model checker for software product lines (SPLs). Variability in software product lines is generally expressed in terms of features, and the number of potential products is exponential in the number of features. Whereas classical model checkers are only capable of checking properties against each individual product in the product line, SNIP exploits specifically designed algorithms to check all products in a single step. This is done by using a concise mathematical structure for product line behaviour, that exploits similarities and represents the behaviour of all products in a compact manner. Specification of an SPL in SNIP relies on the combination of two specification languages: TVL to describe the variability in the product line, and fPromela to describe the behaviour of the individual products. SNIP is thus one of the first tools equipped with specification languages to formally express both the variability and the behaviours of the products of the product line. The paper assesses SNIP and suggests that this is the first model checker for SPLs that can be used outside the academic arena.
The BibTeX data and other interesting links can be found in the publications section.