CRC of ICSE 2012 paper
We submitted the camera ready copy of the ICSE 2012 paper. You can download it here. The abstract is:
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.
Do not expect fancy new tools. Like for the ICSE 2010 paper, the focus of this paper is the theory; in this case, that of simulation in FTS.
In collaboration with Joel Greenyer (Paderborn University, Politecnico di Milano) and Amir Molzam Sharifloo (Politecnico di Milano), we have developed a tool for specifying product lines as scenarios. Using our previous NuSMV extension, the tool is also able to verify the consistency of a specification. See more here.
Paper at ICSE 2012
The technical report posted last year was actually a spin-off from a paper we submitted to ICSE 2012 back then. We just got news that the paper was accepted! ICSE takes place in Zurich this year. The acceptance rate was somewhat higher than in past years (21%). Since we might change the title of the paper for the CRC, we won’t post it yet.
When the CRC is submitted, we will post it here. Stay tuned.
Update. The camera-ready copy is available. Note that the new title is “Simulation-Based Abstractions for Software Product-Line Model Checking”.
Simulation in FTS
We just added a technical report exploring the notions of simulation and abstraction for FTS. You might want to check it out.
Update: snip-r753-20110728
A new version is available for download, the changes wrt. the previous are:
- Added an alias for the if..fi statement: gd..dg, which stands for “guard”. This is mainly to make models easier to understand.
- Updated most of the example models.
Dowload here.
Update: snip-r752-20110630
A new version is available for download, the changes wrt. the previous are:
- Fixed an error in the website.pml example (this was a modification done for a demo which slipped into the last release by accident).
Dowload here.
Talk at ICSE
For those coming to ICSE in Hawaii later this month: I (Andreas) will present our work on symbolic model checking for product lines on Thursday, May 26, 1:45PM, at the model checking session.
Update: snip-r727-20110323
A new version is available for download, the changes wrt. the previous are:
- Added new command line parameter -ospin. It is similar to -spin, but statements whose guard evaluates to false are removed from the model before model checking. The input is thus interpreted as fPromela (not exactly as SPIN would do). This is normally more efficient than -spin.
- Fixed some bugs related to assignment of channel variables to channel IDs.
Dowload here.
Update: snip-r722-20110316
A new version is available for download, the changes wrt. the previous are:
- Added bitwise & bit shifting operators.
- Lifted some restrictions related to the use of labels and gotos inside atomic blocks.
- Fixed two bugs (one related to the -fdlc option, and one related to the timeout keyword).
Dowload here.
CRC of ICSE 2011 paper
We just submitted the camera ready copy of the ICSE 2011 paper. You can download it here. The abstract is:
We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics.
We recently proposed featured transition systems (FTS), a compact representation for SPL behaviour, and defined algorithms for model checking FTS against linear temporal properties. Although they showed to outperform individual system verifications, they still face a state explosion problem as they enumerate and visit system states one by one.
In this paper, we tackle this latter problem by using symbolic representations of the state space. This lead us to consider computation tree logic (CTL) which is supported by the industry-strength symbolic model checker NuSMV. We first lay the foundations for symbolic SPL model checking by defining a feature-oriented version of CTL and its dedicated algorithms. We then describe an implementation that adapts the NuSMV language and tool infrastructure. Finally, we propose theoretical and empirical evaluations of our results. The benchmarks show that for certain properties, our algorithm is over a hundred times faster than model checking each system with the standard algorithm.
Just to be clear, this paper is not related to SNIP; it revolves around symbolic model checking and the tool presented in the paper is a modified version of NuSMV. SNIP, in contrast is a semi-symbolic model checker with an entirely different input language. A paper about SNIP is currently under revision.