by Maurice ter Beek, Henry Muccini and Patrizio Pelliccione
Researchers from the Software Engineering and Architecture group, University of L’Aquila, together with the Formal Methods and Tools group of ISTI-CNR are developing a novel approach that extends and adapts assume-guarantee reasoning to evolving SPLs in order to guarantee resilience against changes in the product environment. The proposal is to selectively verify and test assume-guarantee properties over only the components affected by the changes.
Software Product Lines (SPLs) are part of an SPL Engineering approach aimed at cost effective development of software-intensive products that share an overall reference model. Variety is achieved by identifying variation points as places in the Product Line Architecture (PLA) where specific products are built by choosing between several optional or alternative features.
While many approaches have been proposed to economize on the validation of SPL products by exploiting product similarities and proper variability management, ensuring the resilience of products of an evolving SPL is an ongoing problem. This is illustrated in Figure 1 which shows a model problem, proposed by Paul Clements and colleagues from Carnegie Mellon University.
Figure 1: Evolution requires quality re-evaluation.
“I run the same software in different kinds of helicopters. When the software in a helicopter powers up, it checks a hardware register to see what kind of helicopter it is and starts behaving appropriately for that kind of helicopter. When I make a change to the software, I would like to flight test it only on one helicopter, and prove or (more likely, assert with high confidence) that it will run correctly on the other helicopters. I know I can't achieve this for all changes, but I would like to do it where possible.”
In an SPL context, this problem can be rephrased as: assuming various products (eg helicopters) derived from an SPL have been formally certified, what can be guaranteed for new products obtained from the SPL once one or more core components have been modified?
We took a first step towards a solution by adapting assume-guarantee reasoning, which sees the environment of a component as a set of properties, called assumptions, that should be satisfied for its functioning. If these assumptions are satisfied by the environment, then components in this environment will typically satisfy other properties, called guarantees. By appropriately combining these properties, it is possible to prove the correctness of a system before actually constructing it. Our idea is to permit selective (re-)testing and model checking of assume-guarantee properties on only those SPL components and products affected by the evolution.
Figure 2 contextualizes our work. Components used in the PLA of the SPL of interest are enriched with assume and guarantee properties (top left). The PLA configuration provides context to the assumptions and guarantees: given a component C with its assume-guarantee pair, its environment becomes the sub-architecture connected with C. The process is complicated by the fact that the reasoning is performed on the PLA, including all variation points, rather than on each indivdual product. This means that the assumptions need to be calculated in a smart way taking into consideration the variability management of the components. Once a component evolves (top right), this modification is expected to have an impact on several Product Architectures (PAs), namely each PA that contains the modified component. For instance, when B evolves into B', the assumption and guarantee pairs of both B and B' must be checked.
Figure 2: Contextualization of our work
Our solution thus envisages a combination of regression testing and assume-guarantee testing applied to evolving PLAs. Conceptually, this requires us to better understand two issues.
First, how to extend assume-guarantee testing to evolving architectures. The assume-guarantee pair associated with each component in an architecture is normally used to generate component-specific testing traces which, once evaluated against the appropriate assume-guarantee premise, can show whether the composition of components can produce failures. Assuming a PLA/PA has been tested, the challenge becomes how to apply assume-guarantee reasoning for regression testing the modified PLA/PA (see (1) and (2) in Figure 2, respectively). Second, how to use the relationships between a PLA and its PAs (see (3) in Figure 2) to apply regression testing to the evolved PAs.
In summary, we currently envisage what we call a double regression testing approach, in which an evolved product (eg PA3' in Figure 2) can be tested based on how it regressed from PA3, and based on its relationship with the architecture of its family, PLA' (cf. Figure 2). Our expectation is that this considerably reduces the effort needed to re-analyze products of an SPL upon its evolution.
We are working out the details of our approach, after which we intend to implement it and investigate its effectiveness by applying it to case studies.
Please contact:
Maurice ter Beek
ISTI-CNR, Italy
E-mail:
