What is SPLAnE?

A Software Product Line (SPL) is a development framework to design a family of closely related software products in an efficient and cost-effective manner. Most of the existing state of the art tools in SPL provide analysis operations based only on the requirement specifications (given in the form of Feature Models/Orthogonal Variability Models). The tool SPLAnE (SPL Analysis Engine), which enhances this notion, by allowing analysis operations of software product lines based on (i) SPL requirements in the form of a feature diagram, (ii) core assets of the SPL in the form of a component diagram, and (iii) a traceability mapping between features and sets of components. An important aspect of SPLAnE is that it provides precise implementability between specifications (feature sets) and their implementations (component sets). SPLAnE synthesizes QBF formulae corresponding to the various analysis operations and invokes a QSAT solver (CirQit). Existing tools handle analysis operations by translating them into SAT formulae. SPLAnE has been developed on the state of the art FaMA framework, and accepts its input (SPL requirements, coreassets and traceability) in multiple (about 20) file formats. This framework allows us to plugin various SAT/QSAT solvers in SPLAnE.

Architecture of SPLAnE:

The reasoning process performed by SPLAnE is shown in the Figure. First, SPLAnE takes as inputs a feature model, a traceability relationship and a component model. SPLAnE parser creates the SPL model from this input files. Second, SPLAnE constructs the QBF formula based on the selected analysis operations and encodes it in QPRO format, this is done by SPLAnE translator. QPRO format is a standard input file format in non-prenex, non-CNF form. Later, SPLAnE invokes the QSAT solver CirQit in the back-end to check the satisfiability of the generated QBFs in QPRO format. The choice of the tool is based upon its performance: CirQit has solved the most number of problems in the non-prenex, non-CNF track of QBFEval’10.

SPLAnE Process

The design of SPLAnE makes it possible to use different QSAT solvers. Also, SPLAnE can now work hand by hand with other products based on FaMa such as Betty Tool, which enables the testing of feature models.

Analysis Operations provided by SPLAnE:

Refer the paper Tracing SPLs precisely and efficiently to understand the semantic of below formulae. Analysis Operations

Latest News

SPLAnE v1.0 Released!!

Published on

SPLAnE is available for Ubuntu/Fedora/Mac OS.
SPLAnE can be executed in two mode:
1. SPLAnE-Shell (Click Here to download)
2. SPLAnE-Source code (Click Here to download)

Refer user manual to install and run SPLAnE in shell mode.

Refer user manual for executing SPLAnE through source.

Tutorial for running SPLAnE in Shell mode:

You can download the realistic SPL models from here or the randomly generated SPL models from here.

For this tutorial, we will be explaining SPLAnE on Entry Control Product Line. Open terminal window, and navigate to the unzip folder(SPLAnE folder). Type following on command line:

$java –jar splane.jar


This will open the SPLAnE shell, as show below:

$splane> Type, to display all the available commands.


The screen shot display the available command:

You can either use a command name or abbreviation. You can check the syntax of each command as below:

Now, load the SPL model (feature model, component model, traceability model) for Entry Control Product Line as shown below: (This is required before running any other analysis operations).

On successfully loading the model, check is traceability is complete or not. Traceability should be complete, or other operations may fail.

Check if, feature model and component model is valid or not. Type:

Check if, SPL can generate any product or not ( as below ):

Check for valid Specification:

Alternate way:

Invalid Specification:

Check for valid Implementation:

Alternate way:

Invalid Implementations:

Check if, Implementation implements a feature:

Alternate way, Invalid case:

Check if, the Implementation realize the Specification:

Invalid case:

Check if, the Implementation covers the specifications:

Invalid case:

Checking Soundness and completeness property over SPL:

Check if, component is critical for a given feature:

Check if, element is common in all the product of SPL:

Check if, element is present(live) in atleast one of the product:

Check if, element is not present(dead) in any of the product:

Check if, the Union of two specification, Implementation or product can give any valid specification, Implementation or product respectively:

Check if, the Intersection of two specification, Implementation or product can give any valid specification, Implementation or product respectively:

Publications related to SPLAnE:

1. Tracing SPLs Precisely and Efficiently, Swarup Mohalik, Ramesh S, Jean-Vivien Millo, Krishna Shankara Narayanan and Ganesh Khandu Narwane, 16th International Software Product Line Conference(SPLC '12), Salvador, Brazil.

SPLAnE Team members:

1. Ganesh Khandu Narwane, India
2. José Ángel Galindo Duarte, Spain
3. Krishna S, India
4. David Benavides Cuevas, Spain
5. Jean-Vivien Millo, France
6. Ramesh S, India

Contact below team members for any query:

1. Ganesh Khandu Narwane, India. Email to:ganeshk@cse.iitb.ac.in
2. José Ángel Galindo Duarte, Spain. Email to:jagalindo@us.es