by Maurice ter Beek, Stefania Gnesi and Franco Mazzanti
Researchers from the Formal Methods and Tools group of ISTI-CNR have developed a tool for the computer-aided verification of behavioural variability in product families.
During the last decades, we have witnessed a paradigm shift from mass production to mass customisation in an attempt to serve as many individual customer's needs as possible. A typical example is the production of mobile phones. Software Product Line Engineering (SPLE) translates this paradigm into a software engineering approach aimed at developing, in a cost effective way, a variety of software-intensive products that share an overall reference model, ie that together form a product family. Usually, commonality and variability are defined in terms of features, and managing variability is about identifying variation points in a common family design and deciding which combinations of features are to be considered valid products.
Feature models are widely used for variability management in (S)PLE. A feature model provides a compact representation of all the products of a product family in terms of their features. Figure 1 shows an example feature model inspired by the mobile phone industry, adapted from [1]. The features are represented as nodes in a tree, with different relationships between them. We see that all mobile phones must run software to support calls and to display information on either a basic, a colour or a high resolution screen. The software may include support for a GPS and for media devices such as a camera, an MP3 player or both. Finally, mobile phones including software for a camera must also include software to support a high resolution screen, whereas software for a GPS cannot run on a basic screen.
There is a large body of literature on the computer-aided analysis of feature models to extract valid products and to detect anomalies, ie, undesirable properties such as superfluous or - worse - contradictory variability information (for instance so-called false optional and dead features). These analyses however do not take into account any behavioural variability as only the presence of the software implementing the features is considered, not their temporal ordering. Since software products are often large and complex, and many are used in safety-critical applications in the avionics, railways, or automotive industries, it is unrealistic and practically infeasible to specify - let alone verify - the behaviour of each product individually. Note that our mobile phone example would already require behavioural models for 14 largely identical products.
For this reason, we recently launched a research effort to 1) develop a formal modelling and analysis framework capable of dealing with behavioural variability and 2) provide tools to support this framework with automated verification. This has resulted in the use of Modal Transition Systems (MTSs) as a formal method for describing the combined operational behaviour of an entire product family. An MTS is a Labelled Transition System (LTS) that distinguishes between optional (may) and mandatory (must) transitions. Since MTSs cannot model all variability, we enrich them with an additional set of variability constraints.
We have also developed a tool for the computer-aided verification of behavioural variability in product families, namely VMC (Variability Model Checker). VMC takes as input a high-level description of an MTS together with a set of textual constraints. In our mobile phone example the latter would include “GPS EXC Basic” and “Camera REQ High resolution”.
VMC allows the user to interactively explore an MTS of a product family; model check properties (branching-time temporal logic formulae) over an MTS; visualise the (interactive) explanations of a verification result; generate one, some, or all of the family's valid products (represented as LTSs); browse and explore these; model check whether or not products (one, some, or all) satisfy certain properties; and, finally, help the user to understand why a certain valid product does or does not satisfy specific verified properties by allowing such a product to be inspected individually. Figure 2 shows VMC's capability to model check a temporal logic formula over all valid products of a family.
The core of VMC consists of a command-line version of the model checker and of a product generation procedure. These programs are stand-alone executables written in Ada that can easily be compiled for the Windows, Linux, Solaris, and Mac OS X platforms. These core executables are wrapped with a set of CGI scripts handled by a web server, making it easy to build an html-oriented GUI as well as to integrate graph drawing tools. The development of VMC is ongoing, but a prototypical version is publicly usable online (see the link below) while its executables are available upon request.
Currently, VMC is not targeted at very large families. Its main limitation, however, is the generation of the model from its input language, while its on-the-fly verification engine and advanced explanation techniques are those of the highly optimized family of on-the-fly model checkers developed at ISTI-CNR over the last few decades for verifying formulae in action and state-based branching-time temporal logics derived from the CTL family of logics. The on-the-fly nature of VMC means that in general it is not necessary to generate and explore the whole state space. This feature improves its performance and allows it to deal with infinite-state systems.
Link:
VMC: http://fmt.isti.cnr.it/vmc/
References:
[1] D. Benavides, S. Segura, and A. Ruiz-Cortés: “Automated analysis of feature models 20 years later: A literature review.” Information Systems 35(6) pp. 615-636, 2010. http://dx.doi.org/10.1016/j.is.2010.01.001
Please contact:
Maurice ter Beek
ISTI-CNR, Italy
E-mail:
