We recently designed abstraction techniques to address the state explosion problem well-known in model checking. We distinguish between three kinds of abstractions:
- feature abstraction abstracts variability information to make a given behaviour available to more products;
- state abstraction merges states, and consequently reduces the size of the state space;
- mixed abstraction combines the above two methods.
These advanced verification techniques have been implemented as new prototype variants of ProVeLines. We evaluated their benefits through experiments that tend to show substantial performance gains.
To install and use these new model checking algorithms, first download ProVeLines. Then, download this archive and extract its content into the src directory. Open configure.h and build.sh and do the following:
- To enable feature abstraction, enable the CEGARTRANS option and disable the CEGAR option in configure.h; then uncomment line 92 in build.sh.
- To enable state abstraction, enable the CEGAR option and disable the CEGARTRANS option in configure.h; then uncomment line 93 in build.sh.
- To enable mixed abstraction, enable both CEGARTRANS and CEGAR options in configure.h; then uncomment line 94 in build.sh.
Leave the other options of configure.h disabled. Then follows steps 5 to 7 of the installation guide. You’re done!
The evaluation results can be found here
Our paper entitled “Beyond Boolean Product-Line Model Checking: Dealing with Feature Attributes and Multi-Features” has been accepted at the 35th International Conference on Software Engineering (ICSE ’13).
Here is the abstract:
Model checking techniques for software product lines (SPL) are actively researched. A major limitation they currently have is the inability to deal efficiently with non-Boolean features and multi-features. An example of a non-Boolean feature is a numeric attribute such as maximum number of users which can take different numeric values across the range of SPL products. Multi-features are features that can appear several times in the same product, such as processing units which number is variable from one product to another and which can be configured independently. Both constructs are extensively used in practice but currently not supported by existing SPL model checking techniques. To overcome this limitation, we formally define a language that integrates these constructs with SPL behavioural specifications. We generalize SPL model checking algorithms correspondingly and evaluate their applicability. Our results show that the algorithms remain efficient despite the generalization.
Back in the summer of 2011 we submitted a paper to IEEE Transactions on Software Engineering (TSE). Since this was a regular submission, things went quite slow, but at last, we finally received the acceptance letter! On measures such as impact factor, TSE is consistently ranked as one of the top three Software Engineering journals, so we’re happy.
Here is the abstract:
The premise of variability-intensive systems, specifically in software product line engineering, is the ability to produce a large family of different systems efficiently. Many such systems are critical. Thorough quality assurance techniques are thus required. Unfortunately, most quality assurance techniques were not designed with variability in mind. They work for single systems, and are too costly to apply to the whole system family. In this paper, we propose an efficient automata-based approach to LTL model checking of variability-intensive systems.
We build on earlier work in which we proposed Featured Transitions Systems (FTSs), a compact mathematical model for representing the behaviours of a variability-intensive system. FTS model checking algorithms verify all products of a family at once and pinpoint those that are faulty. This paper complements our earlier work, covering important theoretical aspects such as expressiveness and parallel composition as well as more practical things like vacuity detection and our logic feature LTL. Furthermore, we provide an in-depth treatment of the FTS model checking algorithm. Finally, we present SNIP, a new model checker for variability-intensive systems. The benchmarks conducted with SNIP confirm the speedups reported previously.
You can download a preprint here.
We made our NuSMV extension compatible with the newest version of the famous model-checker. The patch and the installation instructions are found here.
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.
Our paper entitled “Behavioural Modelling and Verification of Real-Time Software Product Line” has been accepted at the 16th International Software Product Line Conference. Here is the abstract:
In Software Product Line (SPL) engineering, software prod- ucts are build in families rather than individually. Many critical software are nowadays build as SPLs and most of them obey hard real-time requirements. Formal methods for verifying SPLs are thus crucial and actively studied. The verification problem for SPL is, however, more complicated than for individual systems; the large number of different software products multiplies the complexity of SPL model- checking. Recently, promising model-checking approaches have been developed specifically for SPLs. They leverage the commonality between the products to reduce the verification effort. However, none of them considers real time.
In this paper, we combine existing SPL verification methods with established model-checking procedures for real-time systems. We introduce Featured Timed Automata (FTA), a formalism that extends the classical Timed Automata with constructs for modelling variability. We show that FTA model-checking can be achieved through a smart combination of real-time and SPL model checking.
The camera-ready copy is available. At the moment, we do not plan to release the prototype tool described in the paper. However, we will implement its functionalities into SNIP in the near future.
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.
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”.