Skip to content
Sep 13 13

Counterexamples Guided Abstraction Refinement for Product-Line Behavioural Models

by mcr

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

Mar 11 13

Paper at ICSE 2013

by mcr

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.

The preprint version is available here. Note that the two variants of SNIP described in this paper are provided as part as ProVeLines.

 

Dec 18 12

Paper in IEEE Trans Software Eng (TSE)

by acs

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.

Oct 10 12

New patch for NuSMV 2.5.4

by mcr

We made our NuSMV extension compatible with the newest version of the famous model-checker. The patch and the installation instructions are found here.

Oct 10 12

Best paper at RE 2012

by mcr

Our paper titled “Efficient Consistency Checking of Scenario-Based Product-Line Specification” has been awarded the best paper award at the RE 2012 conference. The camera-ready copy is found here. More information about the method and the associated tools is found here.

Sep 23 12

Paper in volume 14 of STTT (Int J Softw Tools Technol Transfer)

by acs

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.

Jun 15 12

Paper at SPLC 2012

by mcr

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.

Apr 14 12

CRC of ICSE 2012 paper

by acs

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.

Mar 22 12

Consistency Checking of Scenario-based Product Line Specifications

by mcr

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.

Jan 28 12

Paper at ICSE 2012

by acs

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”.