Detecting Feature Interactions in FORML Models

Abstract

Requirement engineers must know how features (units of functionality) interact, in order to resolve undesired interactions. Model checking has been proposed as an effective method for detecting feature interactions. We propose a method for (1) modelling features as distinct modules (explicating intended interactions with other features), (2) composing feature modules into a system model that preserves intended interactions, (3) translating this rich model into the input language of a model checker, and (4) automatically generating correctness properties whose violations reveal unintended feature interactions.

1 Introduction

A software system is often thought of in terms of its constituent features, where each feature is “an optional or incremental unit of functionality” [24]. Users view features as capabilities (e.g., cut, copy, and paste; Caller ID; Cruise Control). Software developers use features as a criterion for incremental development, to ease system development and evolution, because features can be developed in isolation, in parallel, or by third-party vendors. Feature orientation is particularly relevant in software product lines, in which a family of software products shares a common set of mandatory features and products are differentiated by their variable (optional or alternative) features [23].

The downside of feature orientation is that engineers must consider how features interact when deriving a product from a selection of features. A feature interaction occurs when “one feature affects the operation of [the other] feature” [10]. Some features interact by design: for example, Advanced Cruise Control features are designed to extend and override basic Cruise Control. Other features interact by accident as a consequence of operating in a shared context [16, 19]. To be safe, the engineer needs to be able to specify, understand, control, and reason about the behaviours of features in combination.

Stefania Gnesi is one of the earliest researchers to employ and extend Modal Transition Systems (MTSs) to model and reason about variability in software behaviour. Her group’s contributions have included new variants of MTSs that express different types of variability in behavioural models [14, 15]; logics such as MHML for expressing variability constraints and behaviour properties over MTSs [3, 4]; and reasoners [5, 8] for deriving valid products from product-line models and for analyzing properties of products and product families.

Fig. 1.

FORML analysis process

We aim to emulate Stefania’s work in modelling and analyzing behaviour models of feature-rich software, but we start from the premise of wanting to model features modularly. The Feature-Oriented Requirements Modelling Language (FORML) [21, 22] enables modular specifications of features. Models of features are composed into models of products or a family of products, which can subsequently be model checked. Our work is most similar to work by Stefania and colleagues on detecting conflicts among policies [7]. In their approach, policies and policy actions are expressed as simple UML State Machines, operations on policy rules specify how to compose policy actions (and state machines), and the resulting composite machines can be model checked using the UMC model checker [6].

In this paper, we describe our process of using model checking to detect interactions in FORML models. Figure 1 shows our process: FORML models of distinct features are composed together and translated into the input language of the NuSMV model checker [11]. Importantly, as part of the translation phase, CTL properties [1] for detecting conflicts among features’ actions are also generated, automatically. Generating CTL properties to detect feature interactions is possible because the individual features serve as specifications of how the features ought to behave. That is, CTL properties derived from feature specifications relate to how a feature behaves in isolation; and the violation of a generated property indicates that some behaviour of the feature no longer holds when the feature is composed with other features.

Fig. 2.

World model of MySPL

Fig. 3.

Behaviour model of MySPL

2 Overview of FORML

This section provides a brief overview of FORML. Details can be found in [21].

A FORML model is decomposed into a static model (world model) and a dynamic model (behaviour model). A FORML world model is an ontology of a software product’s environment, expressed as a UML-based concept model. Each concept represents a type of environmental variable. A concept instance is an object that is characterized by attributes, inputs and outputs, and relationships with other objects (e.g., a car has a speed and direction, a road has lanes, and a car travels on a road). The values of world objects comprise the world state. Actions in the behaviour model change the values of world objects. A feature concept is a FORML-specific concept, distinguished by a dashed border, that specifies feature-specific data (attributes, inputs, outputs) that are visible to the environment (e.g., cruisingSpeed is introduced by the Cruise Control feature). A FORML world model includes a feature model [18] that constrains the valid feature configurations of an SPL. Figure 2 shows the world model of a toy SPL called MySPL, consisting of a concept E, having an attribute v of type integer, and three feature concepts, with input events that the features receive from the environment; and a feature model.

A FORML behaviour model comprises a set of feature modules, one for each feature object. Figure 3 shows the feature modules of MySPL’s three features. Each feature module is a set of feature machines and feature-machine fragments. A feature machine is an extended state-machine model, based on the UML state-machine notation [20]. A state may be a basic state or a superstate containing one or more orthogonal regions; each region models a sub state-machine that executes concurrently with the sub machines in sibling regions. A transition between states has a label of the form:

$id: te\ [gc]\ /\ id_1: [c_1] a_1, \ldots , id_n: [c_n] a_n$

where id is the name of the transition; te is an optional triggering event; gc is a boolean guard condition; and $a_1 ... a_n$ are concurrent actions, each with its own name $id_i$ and guard condition $c_i$.

A feature fragment extends a specified feature machine with new or modified behaviours. Specifically, a fragment can add new behaviours at specific points in an existing feature machine:

• A new region added to an existing state

• A new transition (and possibly new states) added to an existing machine.

• A new action added to an existing transition

• A weakening clause that extends the guard condition of an existing transition or action with a disjunct, thereby weakening the guard condition.

A fragment can restrict the behaviour of a feature machine by adding a conjunct, called a strengthening clause, to the guard condition of a transition or action. Strengthening a guard condition results in the condition being satisfied less often, and therefore leads to “removed” behaviours. Lastly, a new feature machine or fragment can replace existing behaviour by specifying a new transition that is enabled under similar conditions as an existing transition, but has higher priority. There is distinct syntax to specify that a new transition has priority over an existing transition; or overrides an existing transition¹. Fragments, transition priorities, and overrides all specify intended feature interactions, in that they express explicit changes to the behaviour of existing features.

3 Composing Behaviour Models

Feature composition in FORML composes feature machines in parallel, and applies fragments (new regions, new transitions, new actions; new clauses in guard conditions; prioritized and overriding transitions) to the feature machines that they extend. The behaviour of a composed model is the concurrent execution of the extended feature machines; each execution step comprises the simultaneous execution of all enabled transitions and their actions [21]. The composition preserves intended interactions specified as weakening/strengthening clauses, and prioritized and overriding transitions. Our analysis does not report intended feature interactions.

Feature composition is commutative and associative [21], which has considerable advantages. For one, engineers do not need to identify an order of composition in order to derive a product from a collection of features. More importantly, it means that the order of composition does not affect analysis results. A third advantage is that new features can be composed with an existing composed model, thereby enabling incremental composition and analysis.

We implemented FORML feature composition [9] using the FeatureHouse framework [2]. FeatureHouse provides a generic framework for the structural composition of feature modules using superimposition. The input to the composer are the feature modules of the selected features; the output is a FORML model representing the composed behaviour model of the software product. The result of composing MySPL’s three features from Fig. 3 is a single state machine (not shown) with three concurrent regions, one for each feature.

4 Translation of FORML to SMV

We analyze FORML models using the NuSMV model checker [11]. NuSMV is a symbolic model checker, which is the best choice when analyzing concurrent models with non-interleaving semantics. Symbolic model verifier (SMV) is the input language to NuSMV.

An SMV model consists of a set of variable declarations (VAR) and a set of variable assignments (ASSIGN). Variables can be of type Boolean, integer sub-ranges (e.g., 0..10), enumerated types (e.g. {on, off}) or an array of any of these types. SMV expression operators include ! (not), $\mid$ (or), & (and), $\rightarrow$ (implies) and $\leftrightarrow$ (iff). Assignment expressions specify variables’ initial values (INIT) at the start of a model’s execution, and their next values (NEXT) in every SMV execution step. A variable can be assigned a specific value or expression over current variable values; a set of values $\{val_1,...,val_n\}$, meaning that the next value is non-deterministically selected from this set; or there can be no assignment, meaning that the next value is non-deterministically selected from the range of values in the variable’s defined type. In this manner, the variable declarations define the model’s state space and the assignments define the model’s transition relation. Macros can be defined (DEFINE) to represent any valid expression. In our translation from FORML to SMV, we use macro definitions instead of variable declarations wherever possible (because macros are not typed and do not contribute to the model’s state space).

SMV modules (MODULE) are used to encapsulate sub-models of variables and assignments. An SMV model can contain several modules, but must have one high-level module called main. An SMV module can be instantiated as a variable in other modules. Given a module instance a, the expression a.x identifies a variable or macro named x inside the instance a. SMV invariants (INVAR) are constraints on SMV variable values. We use invariants to constrain when a transition can execute. SMV comments are preceded by the symbol $--$.

We implemented a translator from FORML to SMV using BSML2SMV [13], which is useful for translating big-step modelling languages (BMSL) [12] into SMV. BSMLs are a family of behaviour modelling languages that have multi-step execution semantics; the family of BSMLs includes UML State-Machines, various statechart variants, and process algebras. We extended BSML2SMV to the execution semantics of concurrently executing transitions that have conflicting actions, and to translate the rich world model of a FORML model.

Fig. 4.

SMV module for WS

Fig. 5.

SMV model of an execution state

4.1 World State (WS) Module

The FORML-to-SMV translator generates an SMV module called WS, which specifies valid world states of a FORML world model. The WS module models the world concepts, their attributes, and associations between these concepts. This module also contains a boolean state variable for each basic state in the FORML composed behaviour model. A state variable has value true whenever it is one of the current execution states of the model. Two instances ws_pre and ws of this module are declared in the snapshot module to represent the current and previous world states. (The previous world state is needed to specify properties for detecting feature interactions.) Fig. 4 shows the WS module for MySPL. WS variables are assigned next values in the snapshot module, described below.

Specifying Bounds for Analysis: Many model checkers, including SMV, verify only finite-state systems. Thus, the engineer must specify bounds on the number of objects of each type in the world model and on the value ranges of variables². For example, the SMV model in Fig. 4 binds the value of attribute E_v to the range 0..2. Specifying a small bound is often sufficient, based on the small-scope hypothesis [17], which claims that a high percentage of bugs can be found by checking a model on all possible inputs within some small bound. One verification strategy is to analyze a model with respect to increasingly larger bounds, until the engineer is satisfied that no bugs are likely to be found deep in the model.

4.2 Snapshot Module

The snapshot module specifies the current execution state of a FORML model. It includes two instances of the WS module: (1) ws, which represents the current world state, and (2) ws_pre, which represents the previous world state. The snapshot module also declares for each transition in the composed FORML model a boolean execution variable, which indicates whether the transition will execute in the next execution step. The values of the execution variables are defined in the state modules, described in the next subsection.

The snapshot module updates all of the WS variables. Consider the snapshot module for our MySPL model, shown in Fig. 5, which includes four types of assignments: (1) The next values of ws_pre variables are always the current values of ws variables. (2) The next value of each state variable is false if it is the source state of an executing transition; true if it is the destination state of an executing transition; and otherwise does not change. (3) The next value of a WS variable reflects the assignments made by the executing transitions. If more than one transition assigns values to the same variable, these actions are merged into the same SMV assignment expression. For example, in MySPL (Fig. 3), there are three transitions $A\{t1\}$, $B\{t1\}$, $C\{t1\}$ that assign E.v to the values 1, 0, and 2, respectively. In the corresponding SMV model (Fig. 5), the next value of E_v depends on the combination of transitions that executes; if more than one transition executes, the value is non-deterministically one of the executing transitions’ assignments³. (4) There are no assignments to the input events A_e1, A_e2 and C_e3 because these are environmental inputs whose values are not controlled by the model; their values are non-deterministically set in each execution step.

Fig. 6.

SMV model of the root state

Fig. 7.

SMV model of a non-basic state

4.3 State Module

An SMV module is generated for each non-basic state and region of the composed behaviour model - including the model’s root state. Each of these modules is passed as a parameter the snapshot instance, ss, declared in the main SMV module. The snapshot parameter gives the state module access to all information defined in the snapshot module. Each state module declares a flag for each transition within its scope (i.e., the state is the lowest-common parent of the transition’s source and destination states); the flag is a boolean macro that indicates whether the transition is enabled with respect to its source state and enabling conditions (events and variables). Each state module also declares two flags (macros) that indicate its own enabledness and execution: the enabled flag indicates whether there is any enabled transition within the scope of that state or any of its descendants, and the exec flag indicates whether any of these enabled transitions will execute in the next execution step.

Figure 6 shows the root state module for MySPL. It declares variables for three regions, one for each of the feature machines in the composed behaviour model. Figure 7 shows the SMV module generated for feature A’s region.

Intended Interaction (Priority): Intended interactions, such as prioritized transitions or overrides, are encoded as invariants expressed over the transitions’ enabled and exec flags. Specifically, if one transition has priority over another, the translator adds an invariant that states that when the higher-priority transition is enabled the lower transition cannot be executed even if the lower-priority transition is enabled.

Fig. 8.

Modified feature C, whose transition has priority over t1 in feature A

For example, Fig. 8 presents a modified feature C whose transition $C'\{t1\}$ has priority over $A\{t1\}$. This is an intended interaction, and is translated to the following SMV invariant:

$$\begin{aligned}&\texttt {INVAR ( C'\_t1\_enabled -> !ss.A\_t1\_exec )} \end{aligned}$$

4.4 Main Module

The SMV main module pulls all of the pieces together. The SMV main module of our running example (in Fig. 9) contains (1) an instance of the snapshot module, (2) an instance of the root-state module, with a snapshot parameter, and (3) the temporal logic properties to be checked. Our translation process automatically generates the properties: one for each transition action. We describe our process for generating interaction-detection properties in the next section.

Fig. 9.

SMV main module

5 Detecting Feature Interactions in FORML

In this paper, we focus on feature interactions that are caused by conflicting actions on shared variables. Note that detecting conflicting assignments is not simply a matter of detecting transitions whose actions effect the same variables – because those transitions might not be reachable, or might never be simultaneously enabled. We need a dynamic analysis, like model checking, to detect realizable conflicts among features’ actions.

A barrier to effective model checking is the need to identify correctness properties to be checked of the model, and to express those properties in temporal logic. In our work, we are able to generate properties for detecting feature interactions automatically from the feature modules. We can do this precisely because of the nature of feature interactions: feature interactions are effectively deviations from how features would behave in isolation. Thus we use features’ FORML behavioural models as specifications of expected behaviours of individual features; and check whether the features’ specified behaviours vary when the features are composed into a product.

5.1 Running Example

This section employs a running example to demonstrate how correctness properties are generated and used to detect interactions. For pedagogical reasons, we consider an SPL called AutoSoft, which has four features that correspond to various basic functions of a car. These features are:

• Ignition Control (IC), responds to commands to turn the vehicle’s ignition on and off (shown in Fig. 11).

• Acceleration control (AC), responds to commands to increase the vehicle’s acceleration (shown in Fig. 12).

• Braking control (BC), responds to commands to decrease the vehicle’s acceleration (shown in Fig. 13).

• Steering control (SC), responds to commands to change the vehicles’s direction (shown in Fig. 14).

Fig. 10.

The AutoSoft World Model

Fig. 11.

The IC feature module

Fig. 12.

The AC feature module.

Fig. 13.

The BC feature module.

Fig. 14.

The SC feature module.

Figure 10 shows the world model for AutoSoft. Figure 15 shows the composed behaviour model that is generated from composing the four features of AutoSoft.

5.2 CTL Property Language

The feature-interaction detection properties to be model checked are expressed as formulae in the Computational Tree Logic (CTL) branching-time temporal logic [1]. Branching-time temporal formulae are evaluated with respect to a particular execution state, based on the set of possible execution paths emanating from the state. Because the future path of the system’s execution is unknown, temporal operators are quantified over the set of possible futures (e.g., a property p is true in some next state or in all next states).

Fig. 15.

Composed behaviour model of AutoSoft

The syntax and semantics for CTL formulas are defined in [1] and are simply summarized below:

• 1. Every propositional variable is a CTL formula.

• 2. If f and g are CTL formulas, then so are: !f, $f \& \!g$, $f\!\mid \!g$, AXf, EXf, A[fUg], E[fUg], AFf, EFf, AGf, EGf.

The symbols ! (not), & (and), and $\mid$ (or) are logical connectives and have their usual meanings. X is the nextstate operator, and formula $EX\phi$ ($AX\phi$) is true in state $s_i$ iff formula $\phi$ is true in some (in every) successor state of $s_i$. U is the until operator, and formula $E[\phi \; U\,\psi ]$ ($A[\phi \; U\,\psi ]$) is true in state $s_i$ iff along some (every) path emanating from $s_i$ there exists a future state $s_j$ at which $\psi$ holds and $\phi$ is continuously true until state $s_j$ is reached. F is the future operator, and $EF\phi$ ($AF\phi$) is true in state $s_i$ iff along some (every) path from $s_i$ there exists a future state in which $\phi$ holds. Finally, G is the global operator, and $EG\phi$ ($AG\phi$) is true in state $s_i$ if $\phi$ holds in every state along some (every) path emanating from $s_i$.

5.3 Generating Feature-Interaction Detection Properties

According to the execution semantics of FORML, if a transition t executes in a given world state, the effects of its actions should be realized in the next world state. If the effects are not realized, it means that some action(s) from other transition(s) have assigned value(s) to some of the same world-model variables, thereby interfering with t’s actions. Such interference can occur among actions performed by a single feature or actions performed by multiple features.

Recall from Sect. 4.2 that, when translating FORML transition actions into SMV assignments, if two or more transitions write to the same world-state variable, the actions need to be merged into the same SMV assignment expression. The outcome is a single (case-based) assignment expression that reflects exactly one transition’s actions if only one transition executes; and that reflects a race condition among actions if several of the transitions execute simultaneously. If these transitions can ever execute together, then a race condition is possible – revealing a feature interaction: an executing transition that loses a race condition has a post-condition that is unsatisfied. Our goal is to specify properties that can detect unsatisfied post-conditions.

We do this by generating automatically a CTL property for each transition action. Each property states that if a transition executes in the current world state, then in the next world state the expected effect of the transition’s actions should be realized. Such properties can be generated solely based on the state-machine model and do not require any user input. We define below the general template for these interaction-detection properties.

Rule 1. For each action of a transition t that assigns a value x to an attribute C_a in the world model, add the following CTL specification to the main module:

This CTL formula states that in All execution paths, it is always (or Globally) true that if the value of t_exec is true, then (in All neXt states) the next value of C_a is equal to the value of x as evaluated in the current world state; if x is an expression, then the next value of C_a is the value of the expression as applied over the current world-state variable values⁴.

Listing 1.1 shows the three example CTL properties that are generated for the three actions: a1 from transition AC_t1, a1 from BC_t1, and a1 from SC_t1. The expressions acceleration_fn and deceleration_fn correspond to the unspecified functions acceleration() and deceleration(), respectively, in Fig. 15. If any of the correctness properties fails, it indicates an interaction among feature actions.

We now show how our approach detects interactions in our AutoSoft example. In Fig. 15, the transitions $AC\{t1\}$ and $BC\{t1\}$ both have actions that assign values to the same variable AutoSoftCar.acceleration. Our translator combines these actions into a single conditional assignment expression that makes a non-deterministic choice if both transitions execute; assigns a unique value if exactly one transition executes; and makes no assignment if neither transition executes:

$$ \begin{aligned}&\texttt {next(ws.AutoSoftCar\_acceleration) := case} \\&~~~~\texttt {AC\_t1\_exec \& BC\_t1\_exec : \{ws.acceleration\_fn,}\\&~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\texttt {ws.deceleration\_fn\};} \\&~~~~\texttt {AC\_t1\_exec : ws.acceleration\_fn;} \\&~~~~\texttt {BC\_t1\_exec : ws.deceleration\_fn;} \\&~~~~\texttt {1 : ws.AutoSoftCar\_acceleration;} \\&\texttt {esac;} \end{aligned}$$

If both transitions execute simultaneously (which is possible because they reside in concurrent regions and do not have conflicting enabling conditions), then AutoSoftCar_acceleration will nondeterministically be assigned to either acceleration_fn or deceleration_fn. In this scenario, only one of the properties P1 or P2 of Listing 1.1 is satisfied. If AutoSoftCar_acceleration is assigned the value of acceleration_fn, property P1 will hold but not P2, and vice versa.

Fig. 16.

Composed behaviour model of AutoSoft, modified to include an intended interaction.

In the real world, this feature interaction represents the case where a driver requests to accelerate and decelerate a vehicle simultaneously, for example by pressing both the gas and brake pedals at the same time. We can resolve this interaction by modifying the model to give one transition priority over the other (in this case, it makes sense to prioritize the transition that decelerates the vehicle) The result is an intended interaction, in which transition BC_t1 can supersede transition AC_t1.

Figure 16 shows a modified version of Feature BC in which transition BC_t1 is explicitly specified to have priority over transition AC_t1. If both transitions are enabled, only BC_t1 can execute. This transition priority is represented in the SMV model as an invariant:

When this invariant is part of the SMV model, it is impossible for AC_t1_exec and BC_t1_exec to both be true at the same time. Therefore, the first case branch in the next(AutoSoftCar_acceleration) assignment never executes; and there is no longer any reported violation of properties P1 and P2.

6 Conclusion

In this paper, we present an approach and tools for detecting feature interactions due to conflicting actions in FORML models. The approach consists of first composing FORML models of features into a composed FORML behaviour model, and then translating the composed model and the FORML world model into the SMV language. As part of the translation process, CTL properties for detecting feature interactions are automatically generated from the translated model. Each CTL property states for some transition action that the post-condition of that action should hold if the transition executes. Lastly, the CTL properties are model checked; any violation of a property indicates a conflict among feature actions. We are currently evaluating the effectiveness of our approach on a case study of 11 automotive drive-assist features from an industrial partner.