-Featured Transition Systems (FTSs) is a popular representation for software product lines: an entire product line is compactly represented as a single transition-machine model, in which feature-specific behaviour is guarded by feature expressions that are satisfied (or not) by the presence or absence of individual features. In previous work, FTS models were monolithic in the sense that the modeller had to construct the full FTS model of the product line in its entirety. To allow for modularity of FTS models, we propose here a language for extending an existing FTS model with new features. We demonstrate the language using a running example and present results about the language's expressivity, commutativity of feature extensions, feature interactions, and resolution of such interactions.
Software product lining is a software development paradigm in which a family of related software products (e.g., similar smart phones, or payroll systems) share a common set of mandatory features and individual products are differentiated by the presence or absence of optional features. Ideally, features are increments of functionality that can be developed independently and combined into products or a product line.
Featured Transition Systems (FTSs) [
As an example, Fig. 1 displays an FTS model of an automated teller machine (ATM). It has a mandatory feature that consists of a cycle of card insertion, PIN entrance, amount specification, cash retrieval, and card retrieval. Hence these transitions will be present in all products. Also shown is an optional “Cancel” feature which allows to cancel transactions, and another optional “Balance” feature which permits the customer to get an account balance. Thus, the transitions belonging to feature Ca will be present only in products which include the Ca feature; the balance-labeled transition from state 2 to state 4 will be present only in products that include the B feature.
In previous work, FTS models were monolithic models of full product lines. There was no means of modelling individual features and composing them into products or product-line models, or of specifying feature increments to an existing product-line model. As such, FTSs could not be the mathematical basis for modelling technologies that support [Ca] cancel
PIN card! 2 amount
3 [Ca] cancel cash
4 [B] balance
Fig. 1. ATM example feature decomposition, composition, or incremental evolution of a product line.
To allow for modularity of FTS models, we propose here a language of feature merge expressions (FMEs) for specifying new feature extensions to an existing FTS model. Specifically, given a base FTS model of mandatory behaviour, an FME is a sequence of FTS transformations that add transitions and states and manipulate feature expressions, thereby embedding new feature-specific behavior into the existing FTS. We show that a relatively small set of FME constructs is sufficiently powerful to express any legal extension of an FTS.
From a methodological point of view, we envision application of FMEs to FTSs to be automatized, and we will show below how to achieve this. Once such automatization is available, FMEs should become a powerful tool for product line specification.
In the following we give a brief overview of FTSs. In Section III, we introduce a preliminary language of simple FMEs and demonstrate its utility on a running example; we conclude that section with a proof of expressivity of the simple language. In Section IV, we extend our preliminary language to include variables, which enable the specification of more general model-transformation rules that (may) apply to multiple locations in an existing FTS. We discuss in Section V the issue of commutativity of feature extensions, interactions among features, and how to use FMEs to specify resolutions to interactions. In Section VI we conclude and describe future directions of this work.
A transition system (TS) S = (S; ; I; T; ) consists of a finite set of states S, a nonempty set of initial states I S, a finite set of actions , and a finite set of transitions T together with a mapping : T ! S S. We write t : s !a s0 to indicate a transition t 2 T with (t) = (s; a; s0). When necessary, we will distinguish input actions from output labels water get in ; in Fig. 1 for example, “card?” denotes the card being input into the ATM, whereas “card!” denotes the card being returned.
Let N be a set of features. A feature expression is a Boolean expression over N ; B(N ) denotes the set of such feature expressions. A product is a subset p N . We denote by tt and ff the universally true, respectively false, feature expressions. For a product p and a feature expression , we write p j= if p satisfies .
A featured transition system (FTS) F = (S; ; I; T; ; ) consists of a TS (S; ; I; T; ) and a mapping : T ! B(N ) which assigns feature guards to transitions.
FTSs are used as compact specifications of product lines, or sets of transition systems depending on products. To be precise, the semantics of an FTS F = (S; ; I; T; ; ) is the mapping JF K from products p N to TSs given by JF K(p) = (S; ; I; T 0; ) with T 0 = ft 2 T j p j= (t)g. That is, the TS JF K(p) contains precisely those transitions from F which are enabled for the product p. Two FTSs F , F 0 are called semantically equivalent, denoted F F 0, if JF K(p) = JF 0K(p) for every product p N .
III. SIMPLE FEATURE MERGE EXPRESSIONS
We want to merge a new feature into an already given FTS. The idea is that we specify rules which may add states to the FTS, add transitions, and modify existing transitions.
We introduce feature merge expressions gradually through a running example. Figure 2 displays a (very) simple vending machine which hands out water to the thirsty traveler, for free. Now we would like to add “Coffee” and “T ea” features to it, noting that these hot beverages do not come for free. To do so, we use a feature merge expression (FME) as follows.
C : T : add 0 coin 2 add 2 coffee 1 add 0 coin 2 add 2 tea 1
We shall give a formal syntax of FMEs below, but we can give an intuitive explanation here. The first rule of the C expression specifies that a new, coin-labeled, transition is to be added to the FTS, leading to a state 2 which does not exist. Hence this state is added to the FTS. The second rule then adds a coffee-labeled transition from state 2 to state 1. The result is displayed in Fig. 3.
The FME for T specifies to add another coin-labeled transition from state 0 to state 2, but as there is one such transition already, the effect is a weakening of the feature guard on this 2 0 2 water get [C] coffee water get
1 The first rule specifies that the coin-labeled transition from state 0 to state 2 is to be strengthened with a feature guard :CC. Hence the CreditCard feature will disable the coin transition, making credit card the only payment option. If we wanted an inclusive CC feature instead, which does not disable coin payment, then we could have omitted this strengthening rule. Also note that strengthening rules are a necessary part of merge expressions; whereas addition rules introduce behaviour, strengthening rules restrict behaviour.
The last two rules of the FME specify that a new state is to be added together with two transitions pertaining to the CC feature. Note the new piece of syntax in the addition rules: the transitions added should only be enabled if either the Coffee or T ea feature are present, so they have to be guarded by the feature expression C _ T . The result of the merge is depicted in Fig. 5.
In general, a feature merge expression for a feature F consists of rules of two types:
addition rules of the form [(C _ T ) ^ CC] card
3 [(C _ T ) ^ CC] PIN 0 2 add s h i a s0 water get [(C _ T ) ^ :CC] coin [C] coffee [T ] tea 1 Fig. 5. Vending machine with Coffee, T ea and CreditCard (the “h i” denotes an optional part) which specify to add a transition (and possibly the states) from s to s0 with label a and feature guard ^ F ; strengthening rules of the form str s a s0 amount
cash Here can be any feature expression, but will usually be only a single feature. In an FME : IE, we call IE an inner expression. Hence the first line above specifies the syntax of merge expressions, whereas the second line specifies the syntax of inner expressions.
We give denotational semantics to FMEs. Let F = (S; ; I; T; ; ) be an FTS and E an FME, then the effect JEK(F ) is a new FTS F 0 which is given by structural induction on E:
JE1; E2K(F ) = JE2K(JE1K(F ))
J : IEK(F ) = JIEK (F ) JIE1; IE2K (F ) = JIE2K (JIE1K (F ))
Jadd s a s0K (F ) = Jadd s tt a s0K (F ) Jadd s a s0K (F ) = (S [ fs; s0g; ; I; T [ ftnewg; 0; 0) where tnew 2= T is a new transition and ( (t)
for t 6= tnew and (s; a; s0) for t = tnew 0(t) = 0(t) = 0(t) = ( (t) ^ (t) ^ for t 6= tnew for t = tnew
with if (t) 6= (s; a; s0) if (t) = (s; a; s0) Jstr s a s0
K (F ) = (S; ; I; T; ; 0)
( (t)
Here the first line shows how to concatenate merge expressions, and the second line gives the rule for how to access an inner expression IE inside an FME E = : IE. The semantics of this inner expression is then dependent on its feature guard , i.e., the meaning of JIEK (F ) depends on .
The third line then shows how to concatenate inner expressions, and the fourth and fifth lines give semantics to addition rules. Note that the second addition rule specifies that a new transition tnew be added to the FTS, whereas the states s and s0 only are added if they do not already exist in S. Proof: Let F = (S; ; I; T; ; ), F 0 = (S0; 0; I0; T 0; 0; 0). By renaming states if necessary, we can assume that S \ S0 = ;. We construct E = tt : IE; IE0, where IE and IE0 are inner expressions.
We first strengthen all transitions in F to make their feature guards unsatisfiable. Write T = ft1; : : : ; tng and define IEj = str (tj ) ff for j = 1; : : : ; n. Let IE = IE1; : : : ; IEn. It is clear that every transition in JIKtt(F ) has unsatisfiable feature guard.
Now we add all transitions in T 0 to J K I Ett(F ). Write T 0 = ft01; : : : ; t0mg and define IEj0 = add 0(t0j ) 0(t0j ) for j = 1; : : : ; m. Let IE0 = IE10; : : : ; IEm0. Then JIE; IE0Ktt(F ) = JEK(F ) is semantically equivalent to F 0.
IV. EXTENDED FEATURE MERGE EXPRESSIONS In order to allow for more generic feature merge expressions, we propose to extend the syntax of FMEs to include variables. We again introduce these through a running example.
Recall the ATM example from Fig. 1, where we for now ignore the Cancel and Balance features. Figure 6 shows the ATM base feature.
Now we would like to add a Receipt feature, which models an ATM where the customer can obtain a receipt after her transaction. Hence R should add a transition labeled rec? from state 4 to a new state 5, asking whether the customer wants a receipt. From state 5, a rec! transition will issue a receipt, leading to another state 6 from which there is a card! transition back to state 0. For the case that the customer does not want a receipt, there should be a transition labeled norec? from state 4 to state 6; also, the R merge expression should strengthen the existing card!-labeled transition.
In order to make our merge expression more generic, we will avoid making explicit reference to existing states like above. Instead, we will specify that the new rec?-labeled transition is to start at the target state of the existing card!labeled transition; similarly, the new card!-labeled transition is to have the same target state as the existing one. This is cash achieved by the following extended feature merge expression (EFME); the result of the merge is displayed in Fig. 7.
R : foreach t labeled card! str t :R
In the above EFME, the line “foreach t labeled card!” loops over all card!-labeled transitions, binding them to the variable t. The lines within the loop’s scope can then access the source state src(t) and the target state tgt(t) of t and its feature guard guard(t).
We would also like to add a M ore feature to the original ATM model, which allows the customer to make more than one transaction in a session. Hence M should add a transition labeled more? back from the start of any card!-labeled transition (this signifying the end of a session) to state 2 and modify other parts of the FTS accordingly. The EFME for M looks as follows, with the ATM+M ore displayed in Fig. 8.
M : foreach t labeled card! str t :M be an EFME, denote by ft 2 T j (t) = (s; a; s0)g = ft1; : : : ; tng all the a-labeled transitions of the FTS under consideration and write (ti) = (si; a; s0i) for all i = 1; : : : ; n. Then the FME translation is : I E10; : : : ; I En0, where each I Ej0 is obtained from I E by the following syntactic replacements: src(t) 7! si tgt(t) 7! s0 i guard(t) 7! (ti)
It is now a natural question to ask how different feature merges interact with each other. This should be phrased as a commutativity question: does it matter whether one feature is merged after another or vice versa, or do the merges commute? Hence we are interested in the question whether application of two FMEs to FTS is commutative, that is, given an FTS F and two FMEs E1, E2, whether JE1; E2K(F ) JE2; E1K(F ).
We will consider the commutativity question on our running ATM example. First, note that the Balance feature (see Fig. 1) does not interact with the Receipt feature: if B is specified using the FME
B : then merging B after R will give the same result as merging B before R. Similarly, B does not interact with M . Hence in these cases, the feature merges are commutative and the merges do not interact.
Much more interesting is the question whether the M ore and Receipt feature merges commute. If we first apply the FME for M and then the one for R to the ATM base, then the result is the FTS ATM+M +R displayed in Fig. 9. As the merge expression for M introduces a second card!-labeled transition into the FTS, the R expression is now applied to two card!-labeled transitions, one from state 4 to state 0 and one from state 7 to state 0. Hence this introduces two copies of the triangle of rec?-, norec?-, and rec!-labeled transitions, one anchored in state 4 and the other in state 7.
Also two new card!-labeled transitions are introduced, one with feature guard :M ^ R and the other with feature guard M ^ R; but as they both connect state 6 to state 0, they can be merged into one card!-labeled transition with feature guard R. Note how this ATM model lets the customer do several transactions using the more?-labeled transition, and only after indicating that she is done (nomore?), the ATM asks whether she wants a receipt.
If we instead apply the FMEs for M and R in the opposite order, i.e., first R and then M , then the result is the FTS ATM+R+M displayed in Fig. 10. Its behaviour is different from ATM+M +R: now the customer is asked whether she wants a receipt after every transaction in a session, instead of collecting one receipt at the end.
Hence the merges of R and M do not commute, but both orders of merging result in reasonable behaviour: ATM+M +R lets the customer do multiple transactions and asks whether it should print a receipt once the customer has done all her transactions; AMT+R+M instead asks whether a receipt is desired after every single transaction. 1 1 3 3 [:R ^ M ] more?
From a designer’s point of view, non-commutativity of feature merges is a sign that feature interactions are taking place and the design needs to be fixed. We propose such a fixed ATM design, called ATM+(M R), in Fig. 11. This FTS lets the customer do several transactions, each time giving her a choice whether to collect a receipt or not. Once she is done, she can collect one more receipt and then get her card back.
In order to fix the interaction of the M and R features, we present an interaction FME which turns both ATM+M +R and ATM+R+M into the fixed ATM+(M R). The following FME carefully adjusts and extends both ATM+M +R and ATM+R+M into ATM+(M R):
We show the complete feature merge expression for the ATM example in Fig. 12. Note that this also includes an FME for the base feature, showing that FMEs can be used to construct FTSs from the bottom up.
We have introduced a simple language of feature merge expressions (FMEs) and shown that these can be used for merging new features into featured transition systems (FTSs). We have shown that FMEs can be used to introduce any legal extension to an FTS. For practical usability, we have introduced extended FMEs (EFMEs), which allow for more generic merge expressions, and shown how to automatically translate EFMEs to simple FMEs.
We have shown a comprehensive example of the use of
FMEs to construct and extend FTSs. For further evaluation,
we plan to implement our feature merge mechanism within
ProVeLines [
We have also seen that feature merges are not always
commutative, and that such (typically undesirable) failures
of commutativity can be resolved using an extra FME.
Noncommutativity of feature merges also appears in other contexts,
in particular in [
We have shown that non-commutativity of feature merges is
related to feature interactions, which opens up connections to
recent work on detecting and fixing feature interactions [
[R ^ :M ] norec? [R ^ M ] card!
[R ^ M ] rec! [R ^ M ] norec?
PIN
cash
[