Efficient static analysis and verification of featured transition systems

Software Product Line Engineering (SPLE) advocates the reuse of components (systems as well as software) throughout all phases of product development. Following this paradigm, businesses today no longer develop single products, but families or product lines of closely- related, customisable products. Upon identifying the relevant features of the product domain, to exploit their commonality and variability, a feature diagram or feature model defines those combinations of features that constitute valid product configurations (Apel et al. 2013). The automated analysis of such variability models has a 30-year history (Benavides et al. 2010; Thüm et al. 2014). Think, e.g., of the detection of anomalies like so called dead or false optional features. Behavioural models with variability, on the other hand, have a shorter history (Fischbein et al. 2006; Fantechi and Gnesi 2007, 2008; Larsen et al. 2007; Gruler et al. 2008; Asirelli et al. 2009; Lauenroth et al. 2009) and they have received considerable attention only during the last decade, following the seminal paper by Classen et al. (2010). SPLs often concern massively (re)used critical software (e.g., in smartphones and the automotive industry), thus it is important to demonstrate their correct behaviour next to their correct configuration.

A Featured Transition System (FTS) is a formal model with variability for capturing the behaviour of all products of an SPL in one compact model (Classen et al. 2013; Cordy et al. 2019); its action-labelled transitions are associated with features that condition their presence in product behaviour. Proving correctness of such models through model checking or testing is challenging. Ideally, the compact structure of the FTS is exploited to reason on the whole SPL at once. Such an all-in-one technique, according to which the behaviour of all products is examined only once simultaneously, is called family-based analysis in contrast to a brute force enumerative product-based analysis, according to which the behaviour of every product is examined individually, one-by-one (Thüm et al. 2014). Over the past decade, FTSs have shown to be amenable to family-based testing and model-checking (Kim et al. 2011; Classen et al. 2012, 2013, 2014; Cordy et al. 2013a; Devroey et al. 2014b, 2016b; ter Beek et al. 2015b, 2017, 2020b; Dimovski et al. 2017; Dimovski and Węsowski 2017; Dimovski2020).

In ter Beek et al. (2019a), we tackled the automated static analysis of FTSs. We defined the following three ambiguities for an FTS: a dead transition (i.e., a featured transition that is unreachable, and thus cannot be executed, in any product); a false optional transition (i.e., a featured transition that can be executed in all products in which its source state is reachable); and a hidden deadlock state (i.e., a state from which a transition can be executed only in some products). We developed an algorithm to detect ambiguities in FTSs (and a means to resolve them), mimicking the well-established anomaly detection for feature models, with a proof of its correctness. The motivations we presented in ter Beek et al. (2019a) were twofold: an ambiguous FTS is often undesired, since it gives an unclear idea of the SPL behaviour, and an unambiguous FTS paves the way for an efficient kind of family-based model checking. We illustrated the latter on a few examples from the literature.

This paper extends ter Beek et al. (2019a) in the following ways.

1. 1.

   We introduce an engineering methodology aimed towards providing feedback to SPL modellers to possibly improve their FTS models and, subsequently, a strategy which offers a number of verification options (cf. Fig. 4). A dead transition in an FTS indicates a modelling error that must be corrected. A false optional transition indicates a redundancy that may be intentional, but resolving it allows for more efficient verification options. A hidden deadlock should be made explicit in the model to improve understanding and to enable an efficient kind of family-based verification—if the deadlocks in the products that are the cause should not be remedied in the first place.

2. 2.

   Driven by the need to improve the practical applicability of our automated static analysis for behavioural ambiguity detection in FTSs, we present a new algorithm (more efficient than that presented in ter Beek et al. (2019a)) for detecting ambiguities in FTSs by reducing the analysis to SAT solving. In addition, we prove its correctness.

3. 3.

   To demonstrate the improved practical applicability, we apply our algorithm to a larger set of benchmark SPL examples than in ter Beek et al. (2019a), including the FTS of the complete mine pump model of Classen(2010, 2011) and that of the Claroline SPL of Devroey et al. (2014a) with over 10,000 transitions, both of which are not tractable with the algorithm presented in ter Beek et al. (2019a). We empirically show the suitability of the new algorithm by means of a clear runtime speedup.

4. 4.

   We capitalise on the promise of an efficient kind of family-based model checking by demonstrating how properties specified in either the well-known Linear-time Temporal Logic (LTL) or in v-ACTLive\(^{\Box }\), a rich action-based and variability-aware fragment of the well-known branching-time Computation Tree Logic (CTL), can be verified (with a linear complexity) directly on an unambiguous FTS (ignoring its feature expressions) such that validity is preserved in all LTSs modelling product behaviour. The preservation of valid v-ACTLive\(^{\Box }\) properties was anticipated in ter Beek et al. (2019a), while the preservation of valid LTL properties was not observed before. These results imply the addition of two efficient verification options to the above mentioned strategy provided to SPL modellers (cf. Fig. 4).

Outline

After mentioning some related work in Section 2 and providing some background in Section 3, we provide our engineering methodology in Section 4 by defining ambiguities in FTSs and providing a means to resolve them. In Section 5, we present the new static analysis algorithm to detect ambiguities in FTSs, based on SAT solving, and prove its correctness. In Section 6, we empirically show the suitability of the new algorithm by applying it to a number of exemplary FTSs from the literature. In Section 7, we show the feasibility of an efficient kind of family-based model checking of FTSs made possible by the static analysis algorithm. Finally, we conclude the paper in Section 8.

Static analysis of FTSs mimics the automated analysis of feature models by defining behavioural counterparts of dead and false optional features (Benavides et al. 2010; Thüm et al. 2014). It is related to static (program) analysis (Nielson et al. 2005; Chess and West 2007), which includes the detection of bugs in the code (like using a variable before its initialisation) but also the identification of code that is redundant or unreachable.

In Kim et al. (2011), conventional static analysis techniques are applied to SPLs that are represented in the form of object-oriented programs with feature modules. The aim is to find irrelevant features for a specific test in order to use this information to reduce the effort in testing an SPL by limiting the number of SPL programs to examine to those with relevant features. In Bodden et al. (2013), several well-known static analysis techniques are lifted to Java-based SPLs without the exponential blowup caused by generating and analysing all products individually. This is achieved by converting such analyses to feature-sensitive analyses that operate on the entire SPL code in one single pass. Basically, if the original analysis reports that a data-flow property holds at a given program statement, then the lifted analysis reports a feature constraint (a logical expression over the set of features) under which that property holds at the given statement.

In Kästner and Apel (2008), static type checking is extended from single programs to an entire SPL (program family) by extending the type system of a subset of Java with feature annotations. This guarantees that whenever the SPL is well-typed, then all possible program variants are well-typed as well, without the need to generate and compile them first.

In Delaware et al. (2009), type-checking for product lines is mechanised and soundness of a constraint-based type system for Lightweight Feature Java (LFJ), an extension of Lightweight Java with support for features, is proved using a full formalisation of LFJ in the Coq proof assistant (Bertot and Castéran 2004).

An encompassing overview of analysis strategies for SPLs, including type checking, static analysis, model checking, and theorem proving, can be found in Thüm et al. (2014) and a recent empirical study on applying variability-aware static analysis techniques to real-world configurable systems is presented in von Rhein et al. (2018).

Family-based model checking of behavioural SPL models provides a means to simultaneously verify multiple behavioural product models in a single run. Properties can be verified with dedicated SPL model-checking tools such as SNIP (Classen et al.2012, 2013, ProVeLines (Cordy et al. 2013a), VMC (ter Beek et al. 2012, 2016a; ter Beek and Mazzanti 2014), fNuSMV (Classen et al. 2014; Dimovski et al. 2019), ProFeat (Chrszon et al. 2018) (for probabilistic model checking), or QFLan (ter Beek et al. 2020a; Vandin et al. 2018) (for statistical model checking), or—through suitable abstractions or encodings—with well-known classical model checkers like SPIN (Dimovski et al. 2015, 2017; Dimovski and Węsowski 2017), PRISM (Dubslaff et al. 2015) (for probabilistic model checking), Maude (Lochau et al. 2016), mCRL2 (ter Beek et al. 2017, 2020b), or NuSMV (Dimovski 2020).

In this paper, we introduce an engineering methodology that enables a kind of family-based model checking for FTSs, according to a strategy that is sketched in Fig. 4 (the part that is not in red). This figure will be discussed in more detail in Sections 4 and 7. The strategy that is sketched is as follows. If (i) the FTS is live, which is the case whenever it has no hidden deadlocks (so, unambiguous FTSs are live), and (ii) the property ϕ to be verified is specified in either LTL or v-ACTLive\(^{\Box }\), then ϕ can be verified directly on the FTS (by ignoring its feature expressions) and if (iii) ϕ holds, this validity is preserved in all LTSs modelling product behaviour, i.e. ϕ holds for all products. If any of these three conditions does not hold, the property needs to be verified with classical (family-based) approaches, such as the ones mentioned above.

The verification methodology depicted in Fig. 4 thus indicates specific cases in which verification of live FTSs reduces to verification of corresponding MTSs and LTSs (which, as we will see, can be obtained straightforwardly by ignoring the feature expressions, and distinguishing necessary and optional transitions in case of MTSs) with a linear complexity.

However, if either (i) the property to be verified is not a v-ACTLive\(^{\Box }\) or LTL formula, or (ii) the result of the verification is false, then the formula needs to be verified with classical family-based model checking or by means of product-based model checking, with an exponential complexity (Classen et al. 2013, 2014).

In this section, we provide some background needed for the sequel. Labelled Transition Systems (LTSs) are the underlying behavioural structure of FTSs.

Definition 1 (LTS)

A Labelled Transition System (LTS) is a quadruple \({\mathscr{L}} = (S,{{{{\varSigma }}}},s_{0},\delta )\), where S is a finite (non-empty) set of states, Σ is a set of actions, s₀ ∈ S is an initial state, and \(\delta \subseteq S\times {{{\varSigma }}}\times S\) is a transition relation.

We call \((s,a,s^{\prime })\in \delta \) an a-(labelled) transition (from source state s to target state \(s^{\prime }\)) and we may also write it as .

We recall classical notions for LTSs that will be used throughout the paper.

Definition 2 (reachability)

Let \({\mathscr{L}} = (S,{{{{\varSigma }}}},s_{0},\delta )\) be an LTS.

A sequence p = s₀t₁s₁t₂s₂⋯ is a path of \({\mathscr{L}}\) if t_i = (s_i− 1,a_i,s_i) ∈ δ for all i > 0; p is said to visit states s₀,s₁,… and transitions t₁,t₂,… and we denote its i th state by p(i) and its i th transition by p{i}.

A state s ∈ S is reachable (via p) in \({\mathscr{L}}\) if there exists a path p that visits it, i.e., p(i) = s for some i ≥ 0; s is a deadlock if it has no outgoing transitions, i.e., \(\nexists (s,a,s^{\prime })\in \delta \), for all a ∈Σ and \(s^{\prime }\in S\).

A transition \(t = (s,a,s^{\prime })\in \delta \) is reachable (via p) in \({\mathscr{L}}\) if there exists a path p that visits it, i.e., p{i} = t, for some i > 0.

Example 1

In Fig. 1, we depict the LTSs \({\mathcal L}_{1}\) and \({\mathcal L}_{2}\), modelling the behaviour of two different coffee machines, adapted from ter Beek et al. (2017, 2019a). Each LTS has actions to insert coins (ins) and to pour either standard (std) or extra large (xxl) coffee upon the insertion of one or two coins, respectively. Clearly all states are reachable and there are no deadlocks.

LTSs \({\mathcal L}_{1}\) and \({\mathcal L}_{2}\) modelling coffee machines

Full size image

FTSs were introduced in Classen et al. (2010) to concisely model the behaviour of all the products of an SPL, modelled as LTSs, in one transition system by annotating transitions with conditions expressing their presence in (product) LTSs. Let \(\mathbb {B} = \{\top ,\perp \}\) denote the Boolean constants true (⊤) and false (⊥), and let \(\mathbb {B}(F)\) denote the set of propositional formulas over a set of features F (i.e., using features as propositional variables). We do not formalise a language for propositional formulas in order to allow the inclusion of all possible propositional connectives but, in particular, we include the constants from \(\mathbb {B}\). The elements of \(\mathbb {B}(F)\) are also called feature expressions. An FTS is an LTS equipped with a feature model and a function that labels each transition with a feature expression. In the following definition, the feature model is represented by the set of its (product) configurations, where each configuration is represented by a Boolean assignment to the features (i.e., selected = ⊤ and unselected = ⊥).

Definition 3 (FTS)

A Featured Transition System (FTS) is a sextuple \(\mathcal {F} = (S,{{{{\varSigma }}}},s_{0},\delta ,F,{\Lambda })\), where S is a finite (non-empty) set of states, Σ is a set of actions, s₀ ∈ S is the initial state, \(\delta \subseteq S\times {{{{\varSigma }}}}\times \mathbb {B}(F)\times S\) is a transition relation, F is a set of features, and \({\Lambda }\subseteq \{ \lambda : F\rightarrow \mathbb {B} \}\) is a set of (product) configurations.

Given a feature expression \(\phi \in \mathbb {B}(F)\), we call \((s,a,\phi ,s^{\prime })\in \delta \) featured transition (labelled with a and limited to configurations satisfying ϕ) and \((s,a,\top ,s^{\prime })\in \delta \) must transition. We may write featured transitions as .

The notions from Definition 2 (path, reachability, deadlock) are carried over to FTSs by ignoring the feature expressions.

A configuration λ ∈Λ satisfies a feature expression \(\phi \in \mathbb {B}(F)\), denoted by λ⊧ϕ, whenever ϕ is valid in the interpretation λ, i.e., the result of substituting the value of the features occurring as variables in ϕ according to λ is ⊤. Thus, by definition, λ⊧⊤.

Without loss of generality, in the sequel we only consider FTSs that do not contain two featured transitions and such that \(\phi \neq \phi ^{\prime }\). Any FTS that does not satisfy this criterion can be transformed into one that does by replacing the two transitions with one featured transition .

Definition 4 (product)

Let \(\mathcal {F} = (S,{{{{\varSigma }}}},s_{0},\delta ,F,{\Lambda })\) be an FTS.

The LTS specified by a particular configuration λ ∈Λ, denoted by \(\mathcal {F}|_{\lambda }\), is called a product of \(\mathcal {F}\). It is obtained from \(\mathcal {F}\) by first removing all featured transitions whose feature expressions are not satisfied by λ (resulting in the LTS \((S,{{{{\varSigma }}}},s_{0},\delta ^{\prime })\), with \(\delta ^{\prime } = \{ (s,a,s^{\prime })\mid (s,a,\phi ,s^{\prime })\in \delta \text { and } \lambda \models \phi \}\)), and then removing all unreachable states and their outgoing transitions.

Given a featured transition \((s,a,\phi ,s^{\prime })\in \delta \), we call \((s,a,s^{\prime })\in \delta ^{\prime }\) its corresponding (LTS) transition. The set of products of \(\mathcal {F}\) is denoted by \(\mathsf {lts}(\mathcal {F})\).

Note that, by construction: (i) each product does not contain unreachable states or transitions, (ii) each must transition of the FTS has a corresponding transition in the products in which it is reachable, (iii) each product does not contain states or actions that were not originally present in the FTS, and (iv) each featured transition has a unique corresponding LTS transition when its source state is reachable.

The feature model expression of \(\mathcal {F}\), denoted by \(\textsc {fm}_{\mathcal {F}}\), is a feature expression that represents Λ (like, e.g., the formula in conjunctive normal form \(\bigvee _{\lambda \in {\Lambda }} (\bigwedge _{f\in F} (\{ f\mid \lambda (f) = \top \}\cup \{ \neg f\mid \lambda (f) = \perp \})\)). Thus, for all \(\lambda : F\rightarrow \mathbb {B}\) it holds that \(\lambda \models \textsc {fm}_{\mathcal {F}}\) if and only if λ ∈Λ. We may write fm instead of \(\textsc {fm}_{\mathcal {F}}\) if no confusion can arise.

Example 2

In Fig. 2, we depict an FTS \(\mathcal {F}\) modelling the behaviour of the two coffee machines from Example 1 as a product line of coffee machines, adapted from ter Beek et al. (2017, 2019a). Imagine that extra large coffee is exclusively available for the American market, while standard coffee is exclusively available for the European market. To this aim, \(\mathcal {F}\) has transitions labelled with features $ and €, representing products for either the American or the European market, respectively, and a must transition that must be present in every product. Its feature model, depicted in Fig. 3(left), can be represented by the feature expression \(\textsc {fm}_{\mathcal {F}} = {\$}\oplus \text{\texteuro} \), where ⊕ denotes the exclusive disjunction operation. Hence the product configurations of \(\mathcal {F}\) are Λ = {λ₁,λ₂}, where λ₁($) = ⊥, λ₁(€) = ⊤, λ₂($) = ⊤, and λ₂(€) = ⊥. The LTSs \(\mathcal {F}|_{\lambda _{1}}\) = \({\mathcal L}_{1}\) and \(\mathcal {F}|_{\lambda _{2}} = {\mathcal L}_{2}\), depicted in Fig. 1, model the behaviour of the only two products of \(\mathcal {F}\): configuration λ₁ for the European market and λ₂ for the American market.

FTS \({\mathcal {F}}\) modelling a product line of coffee machines

Full size image

Feature models of product line of coffee machines (left), with a dead feature (middle), and with a false optional feature (right)

Full size image

Parallel composition of FTSs is equal to the classical parallel composition of LTSs modulo projection (Classen 2011, 2013). Intuitively, parallel composition partially interleaves the transitions of the LTSs, permitting asynchronous execution of their actions, except for those with shared actions, which are synchronised, thus only permitting execution of their actions at the same time. In case of FTSs, the feature expressions of synchronised transitions are conjuncted,^{Footnote 1} while each interleaved transition simply maintains its feature expression (Classen 2011; Classen et al. 2013).

When applying automated analysis of feature models, the better known analysis operations that are typically being performed concern the detection of anomalies (cf., e.g., Benavides et al. 2010; Thüm et al. 2014). These anomalies reflect ambiguous or even contradictory information. Examples include so-called dead and false optional features. A feature is dead if it is not contained in any product configuration of the FTS, whereas it is false optional if it is contained in all product configurations of the FTS even though it is not a designated mandatory feature. Such anomalies are typically due to an incorrect use of cross-tree constraints. Consider the feature models depicted in Fig. 3. The one on the left corresponds to the feature model expression $ ⊕€ from Example 2 and it has neither dead nor false optional features. The one in the middle corresponds to the feature model expression $ ∧ ($ ↑€), where ↑ is the negation of conjunction (a.k.a. not and), and it has a dead feature €, indicated in red, because this optional feature is excluded by the mandatory feature $ and thus never present. The feature model on the right, finally, corresponds to the feature model expression \( {\$}\wedge ({\$}\rightarrow \text{\texteuro} )\), meaning that € is false optional, indicated in red, because it is required by the mandatory feature $ and as such always present.

In this section, we formalise equivalent notions in a behavioural setting, by adapting the above notions to (featured) transitions of an FTS (Section 4.1). Furthermore, we define ambiguous FTSs and we show how to transform any ambiguous FTS into an unambiguous one (Section 4.2). This constitutes our envisioned engineering methodology, which is sketched in Fig. 4 (the top-right red part) together with a number of verification options (the part of Fig. 4 that is not red) organised in a strategy that was briefly outlined in Section 2 and which will be discussed in more detail in Section 7. This engineering methodology improves the clarity of behavioural SPL models, which is one of the contributions of this paper.

Engineering methodology (top-right red part) and verification options (not in red)

Full size image

4.1 Behavioural ambiguities

Recall from Definition 4 that all states of a (product) LTS of an FTS are reachable from the initial state.

Definition 5 (dead transition)

We say that a transition (of an FTS) is dead to mean that in all the FTS’s products the corresponding (LTS) transition is not reachable.

Clearly, since an FTS is intended to compactly represent the behaviour of all products of a product line, a dead transition in an FTS indicates a modelling error that must be signalled to the modeller so it can be corrected. Such correction can mean removing the transition or changing its feature expression.

Definition 6 (false optional transition)

We say that a transition (of an FTS) is false optional to mean that: (i) it is not dead, (ii) it is not annotated with the feature expression ⊤, and (iii) its corresponding (LTS) transition is present in all the FTS’s products in which its source state is present.

Definition 6 is a slightly revised version of that of ter Beek et al. (2019a, Def. 3.2), in which condition (i) was not explicitly required. Note that condition (iii) does not imply condition (i). In fact, condition (i) requires the source state of the considered transition to be present (i.e., reachable) in at least one product of the FTS, which is not guaranteed by condition (iii).

A false optional transition in an FTS indicates a redundancy, in the sense that the associated feature expression can be replaced by ⊤ without changing the behaviour of any of the products of the product line. This redundancy may be intentional syntactic sugar, to underline the fact that the considered transition is part of the behaviour of those product configurations that satisfy the feature expression, but otherwise it may be useful for the modeller to know. Moreover, as we will see in Section 7, substitution of the feature expression with ⊤ allows for more efficient verification because it results in one more must transition, and thus one less feature expression to be evaluated.

Example 3

In Fig. 5(left), we depict an FTS \(\mathcal {F}\) with features f₁ and f₂ and feature model fm = f₁ ⊕ f₂. The LTSs \(\mathcal {F}|_{\lambda _{1}}\) and \(\mathcal {F}|_{\lambda _{2}}\), depicted in Fig. 5(middle and right), model the behaviour of its two valid product configurations: λ₁ = {f₁} and λ₂ = {f₂}. We immediately see that transition is dead and transition is false optional.

FTS \(\mathcal {F}\) and its product LTSs \(\mathcal {F}|_{\lambda _{1}}\) and \(\mathcal {F}|_{\lambda _{2}}\)

Full size image

An important safety property of systems concerns deadlock freedom, i.e., the system should not reach a state in which no further action is possible, thus guaranteeing progress or liveness (Alpern and Schneider 1985; Manna and Pnueli 1995). In case of configurable systems (like FTSs) this notion can be extended to guaranteeing liveness for each product variant (LTS).

In order to express this notion in the context of FTSs, we introduce the following definition (recall from Section 3 that a state of an FTS is said to be a deadlock if it has no outgoing transitions).

Definition 7 (hidden deadlock state)

We say that a state (of an FTS) is a hidden deadlock to mean that: (i) it is not a deadlock in the FTS, whereas (ii) it is a deadlock in at least one of the FTS’s products (LTSs).

Note that, because of condition (ii) in Definition 7, hidden deadlock states of an FTS are present in one or more of its (product) LTSs.

A hidden deadlock in the FTS should definitely be signalled to the modeller, so it can be checked whether the deadlocks in the LTSs should be remedied. If they should not, i.e., if the deadlocks in the LTSs are intended or unavoidable, then this should be made explicit in the FTS to improve understanding. Moreover, as we will see below, this enables a kind of family-based verification.

Definition 8 (ambiguous FTS)

We say that an FTS is ambiguous to mean that: (i) at least one of its states is a hidden deadlock, or (ii) at least one of its transitions is dead or false optional.

Example 4

It is easy to see that state of the FTS \(\mathcal {F}\) depicted in Fig. 5(left) is a hidden deadlock state, because is a deadlock in the LTS \(\mathcal {F}|_{\lambda _{1}}\). Indeed, \(\mathcal {F}\) is an ambiguous FTS (cf. also Example 3).

Now consider the ambiguous FTS \(\mathcal {F}^{\prime }\) depicted in Fig. 6(left) with features f₁ and f₂ and feature model fm = f₁ ⊕ f₂.

FTS \({\mathcal {F}}^{\prime }\) and its product LTSs \(\mathcal {F}^{\prime }|_{\lambda _{1}}\) and \(\mathcal {F}^{\prime }|_{\lambda _{2}}\)

Full size image

The LTSs \(\mathcal {F}^{\prime }|_{\lambda _{1}}\) and \(\mathcal {F}^{\prime }|_{\lambda _{2}}\), depicted in Fig. 6(middle and right), model the behaviour of its two valid product configurations: λ₁ = {f₁} and λ₂ = {f₂}. Similar to Example 3, transition is dead. However, transition is no longer false optional, since it is indeed not present in \(\mathcal {F}^{\prime }|_{\lambda _{2}}\) even though its source state s₁ is reachable in that LTS. Moreover, not only state is a hidden deadlock (for the same reason as above) but so is state , since it is a deadlock in \(\mathcal {F}^{\prime }|_{\lambda _{2}}\). Hence also \(\mathcal {F}^{\prime }\) is ambiguous.

In Definition 8, an FTS is said to be ambiguous if it has a hidden deadlock state or a dead or false optional transition. We can imagine further ambiguities. For instance, consider for a moment an FTS with the two ‘nearly’ duplicate transitions and (such FTSs are generally not considered in this paper, cf. Section 3). Then the second transition is redundant, since the validity of its feature expression implies that of the first transition, meaning that the second transition adds no behaviour. This clearly represents a kind of ambiguity, since looking at that second transition in isolation it would seem that execution of a requires the presence of features f and g, while actually the presence of f suffices.

Clearly, it is unlikely that systems over a certain size are modelled as single monolithic FTSs. Typically, (large) systems are designed in a modular way, as a composition of (smaller) components. We will see examples of such systems in Section 6. Our engineering methodology goes into that direction. The feedback that our analysis provides to the modellers offers them a means to revise their (small) models before composing these models to form (larger) systems.

4.2 Resolving ambiguities

The initial part of our engineering methodology (i.e., the top-right red part of Fig. 4) concerns checking for ambiguities. Next to providing feedback to the modeller, it is important to know how to resolve ambiguities in an FTS. A dead transition could simply be removed, but this might not be the right thing to do, since the modeller may simply have made a mistake in the behavioural model or in the feature model. Likewise for a false optional transition, which however could also be intentional, to make explicit that the (corresponding) transition is part of the behaviour of those product configurations that satisfy the associated feature expression. Finally, a hidden deadlock should either be made explicit in the FTS, which can be done by adding a deadlock state to the FTS, or the deadlocks in the LTSs should be remedied—again by changing the behavioural model or the feature model. Hence, based on the detailed feedback obtained, the modeller can iteratively improve and check the FTS until the FTS is either unambiguous or ambiguous, but such that it is the FTS as intended by the modeller.

In the latter case, according to the above recipes, any ambiguous FTS can be straightforwardly turned into an unambiguous FTS by the following transformation:

1. 1.

   remove the dead transitions;

2. 2.

   turn the false optional transitions into must transitions; and

3. 3.

   make explicit the hidden deadlocks by adding to the set of states S of the FTS a distinguished deadlock state s_‡∉S and, for each hidden deadlock state s, adding a new transition (which we call a deadlock transition) with s as source, s_‡ as target, and labelled by a distinguished action ‡∉Σ and by a feature expression that negates the disjunction of the feature expressions of all its source state’s outgoing transitions.

Note that step (3) needs to be performed only for those hidden deadlock states that have not yet become explicit deadlock states upon the removal of dead transitions in step (1).

Example 5

In Fig. 7(left), we depict an unambiguous FTS \(\mathcal {F}_{*}\) that was obtained by transforming the ambiguous FTS \(\mathcal {F}\) of Fig. 5. We removed dead transition and false optional transition was turned into must transition . Note that in this case there was no need to add a deadlock transition from the hidden deadlock state to a newly added explicit deadlock state, since has become an explicit deadlock state in the FTS upon removal of the dead transition .

Unambiguous FTSs obtained from the FTSs of Figs. 5 and 6

Full size image

In Fig. 7(right), we depict an unambiguous FTS \(\mathcal {F}^{\prime }_{*}\) that was obtained by transforming the ambiguous FTS \(\mathcal {F}^{\prime }\) of Fig. 6 as follows. We removed the dead transition and we added the deadlock transition from the hidden deadlock state to the newly added explicit deadlock state . Note that in this case, without adding this deadlock transition, state would have remained a hidden deadlock state in \(\mathcal {F}^{\prime }_{*}\).

Note that the addition of explicit deadlock states and transitions does not preserve bisimilarity (nor trace equivalence), which means that resolving the ambiguities does not guarantee that the properties of the original FTS are maintained.^{Footnote 2} However, if a modeller decides to resolve ambiguities in an FTS (as signalled by our static analysis) through the introduction of explicit deadlock states and transitions, then even though the resulting FTS is no longer bisimilar to the original one, it has gained in clarity. Furthermore, as anticipated earlier, a kind of family-based verification on the improved FTS becomes available to the modeller, according to the strategy outlined in Fig. 4.

As said before, an ambiguous FTS may be due to a mistake of the modeller in defining the feature model, in particular in the case of large feature models with many cross-tree constraints. Here we provide a small example, leaving more meaningful examples to Section 6.

Example 6

Consider again the FTS \(\mathcal {F}\) depicted in Fig. 5(left), but now with feature model \(\textsc {fm} = f_{1}\rightarrow f_{2}\), i.e. the presence of feature f₁ requires that of f₂. In this case, the LTS \(\mathcal {F}|_{\lambda _{1}}\) has two further a-transitions, viz. loops in states s₀ and s₂, meaning that \(\mathcal {F}\) no longer exhibits neither dead transitions nor hidden deadlock states—only the false optional transition remains (cf. Examples 3 and 4).

In this section, we present an algorithm to detect behavioural ambiguity. It relies on expressing the conditions of being a hidden deadlock state, a dead transition, or a false optional transition in an FTS as propositional formulas (in which the names of the FTS’s features, states and transitions are used as propositional variables), thus reducing FTS ambiguity detection to solving a set of SAT problems (Cook 1971) (i.e., to decide whether a given propositional formula is satisfiable). While SAT solving is well known to be NP-complete, SAT solvers are widely used for all kinds of static analysis on feature models with a surprising effectiveness even for models with hundreds of thousands of clauses and tens of thousands of variables (Mendonca et al. 2009; Liang et al. 2015).

To this aim, our implementation exploits an automatic SAT solver. SAT solving is an active field of research (Heule et al. 2021; Bjørner et al. 2015; Hutter et al. 2017; Audemard et al. 2016) and tools exist that compute, more or less efficiently, a solution for an input formula, or fail if the formula is not satisfiable. Hence, by feeding the formula encoding an ambiguity question to a SAT solver, we can obtain an answer to it. In our implementation, we use the Z3 SMT solver (de Moura and Bjørner 2008) (that includes a SAT solver) developed by Microsoft Research and freely available under the MIT license. The python code of our implementation is publicly available (ter Beek et al. 2019c); it accepts FTSs in the format .dot as input and all example models used in the remainder of this paper are provided.

5.1 FTS representation

Our algorithm assumes that the considered FTS is represented by the global data structure fts that includes four fields:

1. 1.

   states stores the set of all states in the FTS;

2. 2.

   transitions stores the set of all transitions in the FTS;

3. 3.

   initial stores the initial state of the FTS;

4. 4.

   fm stores the formula fm (introduced before Example 2 in Section 3), which is a formula in \(\mathbb {B}(F)\) that represents the feature model of the FTS.

Each state is represented by a data structure that includes three fields:

1. 1.

   in_trs stores the set of incoming transitions of this state;

2. 2.

   out_trs stores the set of outgoing transitions of this state;

3. 3.

   hdead is a Boolean flag used to record whether this state is a hidden deadlock.

Each transition is represented by a data structure that includes four fields:

1. 1.

   bx stores the feature expression labelling the transition, i.e., a propositional formula in \(\mathbb {B}(F)\);

2. 2.

   source stores the source state of the transition;

3. 3.

   dead is a Boolean flag used to record whether this transitions is dead;

4. 4.

   false_opt is a Boolean flag used to record whether this transitions is false optional.

The Boolean flags in each state (field hdead) and transition (fields dead and false_opt are used to record the results of the analysis (i.e., the output of the algorithm); their initial values are immaterial.

5.2 Propositional formulas expressing the conditions to be checked

Let \(\mathcal {F} = (S,{{{{\varSigma }}}},s_{0},\delta ,F,{\Lambda })\) be an FTS. Let T be the set of the names of the transitions of the FTS. In this section, we introduce propositional formulas on \(\mathbb {B}(F\cup S\cup T)\) that express the conditions of being a hidden deadlock state, a dead transition, or a false optional transition in the FTS.

Recall that an interpretation for a propositional formula in \(\mathbb {B}(F\cup S\cup T)\) is a function \(\mathcal {I}:(F\cup S\cup T) \longrightarrow \{\top ,\perp \}\). We say that a state or transition is selected in an interpretation to mean that the associated propositional variable gets value ⊤ and, on the other hand, we say it is deselected in an interpretation to mean that the associated propositional variable gets value ⊥.

Notation 1

For the sake of simplicity, we abuse the notation of data structures for states and transitions (cf. Section 5.1). We use fts.states as an alternative name for S, and use fts.transitions as an alternative name for T. We use fts.initial to refer to the initial state s₀, use s ∈fts.states and s =t.source (where t ∈ T) to refer to the corresponding state (an element of S), and use t ∈fts.transitions, t ∈ s.in_trs, and t ∈ s.out_trs to refer to the corresponding transition (an element of T).

Let inner_states denote the set fts.states∖{fts.initial}. An initial path is a path that starts from the initial state.

We first introduce some propositional formulas that, together with the formula fts.fm, allow us to formalise the conditions that grasp the initial paths in the FTS’s products.

• ϕ_initial is the formula fts.initial (i.e., the name of the initial state). This formula is valid in an interpretation \(\mathcal {I}\) iff \(\mathcal {I}\) selects the initial state.

• ϕ_inner is the formula \(\bigwedge _{s\in \texttt {inner\_states}} (s\!\Rightarrow \! \texttt {atLeastOneTransition-}\) Of(s.in_trs)), where atLeastOneTransitionOf(X) is a placeholder for \(\bigvee _{t\in X}\) (t.bx ∧ t ∧ t.source). This formula is valid in an interpretation \(\mathcal {I}\) iff \(\mathcal {I}\) selects only states that are reachable via selected transitions, with valid (in \(\mathcal {I}\)) feature expressions, that are outgoing from selected states.

• ϕ_single is the formula \(\bigwedge _{s\in \texttt {fts.states}} \texttt {atMostOneOf}(s.\texttt {out\_trs})\), where atMostOneOf(X) is a placeholder for \(\bigwedge _{t\in X} t\Rightarrow (\bigwedge _{t^{\prime }\in X\setminus \{t\}}\neg t^{\prime })\). This formula is valid in an interpretation \(\mathcal {I}\) iff \(\mathcal {I}\) selects at most one outgoing transition, for each state (selected or not).

• end(s) is the formula \(s \land (\bigwedge _{t\in s.\texttt {out\_trs}} \neg t)\). This formula is valid in an interpretation \(\mathcal {I}\) iff \(\mathcal {I}\) selects the state s and deselects all outgoing transitions from that state.

Next, we focus our attention on the conjunction of the above formulas.

• is_useful_state(s) is the formula fts.fm∧ ϕ_initial∧ ϕ_inner∧ ϕ_single∧end(s). This formula is satisfiable (i.e., valid in some interpretation \(\mathcal {I}\)) iff in at least one LTS product there is a simple path (i.e., a path with no repeated states) that starts from the initial state and ends in s.^{Footnote 3}

Example 7

Consider the FTS on the right.

It has no features and just one product configuration (represented by the mapping from the empty set to \(\mathbb {B}\)) which yields the LTS consisting of the initial state s₀. Therefore, fts.fm = ⊤. States s and s₁ are not useful (since they are not reachable from s₀) and, accordingly, the formulas is_useful_state(s) and is_useful_state(s₁) are not satisfiable. To see this, let t be the transition from s₁ to s and let t₁ be the transition from s₁ to s₁.

• To satisfy is_useful_state(s) requires to assign ⊤ to s (because end(s) must be satisfied), which in turn requires to assign ⊤ to both t and s₁ (because ϕ_inner must be satisfied), which in turn requires to assign ⊥ to t₁ (because ϕ_single must be satisfied, viz. only t can exit s₁), which in turn implies that ϕ_inner cannot be satisfied (because at least one transition has to enter s₁) and therefore is_useful_state(s) cannot be satisfied.

• To satisfy is_useful_state(s₁) requires to assign ⊤ to s₁ and ⊥ to t₁ (because end(s₁) must be satisfied), which in turn implies that ϕ_inner (and therefore is_useful_state(s₁)) cannot be satisfied.

We can straightforwardly define the formulas for checking the behavioural ambiguities by exploiting the formula is_useful_state(s).

• exists_deadlock(s) is the formula \(\text {is\_useful\_state}(s) \land \bigwedge _{t\in s.\texttt {out\_trs}} \neg t.\texttt {bx}\). This formula is satisfiable iff, in at least one LTS product, the state s is a deadlock—thus if s is not a deadlock in the FTS, then s is a hidden deadlock (cf. Definition 7).

• is_not_dead_transition(t) is the formula is_useful_state(t.source)∧ t.bx. This formula is satisfiable iff the transition t is not dead (cf. Definition 5).

• may_be_opt_transition(t) is the formula is_useful_state(t.source) ∧¬t.bx. This formula is satisfiable iff the LTS transition corresponding to transition t (of the FTS) is not present in at least one of the FTS’s products in which its source state is present—thus if t is not dead, then t is not false optional (cf. Definition 6).

Example 8

Consider the FTS \(\mathcal {F}\) of Example 3. Let t₀, t₁, t₂, and t₃ be the transitions , , , and , respectively.

We have that the formula is_not_dead_transition(t₃) is not satisfiable (therefore t₃ is dead) and the formula exists_deadlock(s₂) is satisfiable (therefore state s₂ is a hidden deadlock).

Moreover, the formula is_not_dead_transition(t₂) is satisfiable (therefore t₂ is not dead) and the formula may_be_opt_transition(t₂) is satisfiable (therefore t₂ is false optional).

Consider the FTS \(\mathcal {F}^{\prime }\) of Example 4. Let t₀, t₁, t₂, and t₃ be the transitions , , , and , respectively.

We have that the formula is_not_dead_transition(t₃) is not satisfiable (therefore t₃ is dead). Moreover, both formulas exists_deadlock(s₁) and exists_deadlock(s₂) are satisfiable (therefore both s₁ and s₂ are hidden deadlocks).

We denote by \(\lambda _{\mathcal {I}}\) the restriction of the interpretation \(\mathcal {I}\) to features.

The following lemma formally states the meaning of the five components of the formula is_useful_state(s).

Lemma 1

Let fts be the global data structure that represents the FTS \(\mathcal {F} = (S,{{{{\varSigma }}}},s_{0},\) δ, F,Λ) and let \(\mathcal {I}\) be an interpretation. Then

1. 1.

   \(\mathcal {I} \models {} \texttt {fts.fm}\) iff \(\lambda _{\mathcal {I}}\in {\Lambda }\).

2. 2.

   \(\mathcal {I} \models {} \phi _{\texttt {initial}}\) iff \(\mathcal {I}(\texttt {fts.initial})= \top \).

3. 3.

   \(\mathcal {I} \models {} \phi _{\texttt {inner}}\) iff, for all s ∈inner_states, if \(\mathcal {I}(s)=\top \) then there is at least a transition t ∈ s.in_trs such that: \(\mathcal {I} \models {} t.\texttt {bx}\), \(\mathcal {I}(t)=\top \), and \(\mathcal {I}(t.\texttt {source})=\top \).

4. 4.

   \(\mathcal {I} \models {} \phi _{\texttt {single}}\) iff, for all s ∈inner_states, there is at most one transition t ∈ s.out_trs such that \(\mathcal {I}(t)=\top \).

5. 5.

   \(\mathcal {I} \models {} \texttt {end}(s)\) iff, \(\mathcal {I}(s)= \top \) and \(\mathcal {I}(t)=\perp \), for all t ∈ s.out_trs, where s ∈fts.states.

Proof

Straightforward. □

The next lemma formally states the meaning of the formula is_useful_state(s).

Lemma 2

Let fts be the global data structure that represents the FTS \(\mathcal {F} = (S,{{{{\varSigma }}}},s_{0},\) δ, F,Λ) and let \(s^{\prime }\) be a state of \(\mathcal {F}\).

Then the formula \(\texttt {is\_useful\_state}(s^{\prime })\) is satisfiable iff there are an interpretation \(\mathcal {I}\) and an initial path P of \(\mathcal {F}\) ending in \(s^{\prime }\) such that \(\lambda _{\mathcal {I}}\in {\Lambda }\) and

1. 1.

   \(\mathcal {I}(s)=\top \), for each state s visited by P, and

2. 2.

   \(\mathcal {I}(t)=\top \) and \(\lambda _{\mathcal {I}} \models {}t.\texttt {bx}\), for each transition t visited by P.

Proof

We consider first the direction from right to left. Let \(\mathcal {I}\) be an interpretation and P an initial path of \(\mathcal {F}\) ending in \(s^{\prime }\) such that \(\lambda _{\mathcal {I}}\in {\Lambda }\) and conditions (1) and (2) hold. Consider the interpretation \(\mathcal {I}_{0}\) that maps to ⊥ all the states and transitions that are not in P and behaves as \(\mathcal {I}\) on all other arguments. Then it is immediate to check that \(\mathcal {I}_{0}\models {} \texttt {is\_useful\_state}(s^{\prime })\) holds (i.e., \(\texttt {is\_useful\_state}(s^{\prime })\) is satisfiable).

Consider now the other direction. Let \(\mathcal {I}^{\prime }\) be an interpretation satisfying \(\texttt {is\_useful\_state}(s^{\prime })\), i.e., such that \(\mathcal {I}^{\prime }\models {} \texttt {fts.fm}\), \(\mathcal {I}^{\prime }\models {}\phi _{\texttt {initial}}\), \(\mathcal {I}^{\prime }\models {} \$\phi _{\texttt {inner}} \), \(\mathcal {I}^{\prime }\models {} \phi _{\texttt {single}} \), and \(\mathcal {I}^{\prime }\models {} \texttt {end}(s^{\prime })\) hold.

Immediately, \(\lambda _{\mathcal {I}^{\prime }}\in {\Lambda }\) follows from \(\mathcal {I}^{\prime }\models {}\texttt {fts.fm}\), while \(\mathcal {I}^{\prime }(\text {fts.initial})= \top \) and \(\mathcal {I}^{\prime }(s^{\prime })=\top \) follow from \(\mathcal {I}^{\prime }\models {} \phi _{\text {initial}}\) and \(\mathcal {I}^{\prime }\models {} \texttt {end}(s^{\prime })\), respectively.

Then the proof follows by induction on the number n of states selected by \(\mathcal {I}^{\prime }\) (note that n must be at least one, since fts.initial is always selected).

• If n = 1, then we are selecting only one state, i.e., \(s^{\prime }\) and the initial state coincide. Hence, the initial path is just \(s^{\prime }\) and the proof that conditions (1) and (2) hold is immediate.

• Let n > 1. If \(s^{\prime }\) is the initial state, then the proof is immediate (as for the case n = 1). Thus, let \(s^{\prime }\) be different from the initial state. We know that \(s^{\prime }\) is selected in whatever interpretation satisfying \(\texttt {is\_useful\_state}(s^{\prime })\). By Lemma 1(3), we know that there are m ≥ 1 transitions {t₁,…,t_m}∈ s.in_trs such that \(\mathcal {I}^{\prime } \models {}t_{i}.\texttt {bx}\), \(\mathcal {I}^{\prime }(t_{i})=\top \), and \(\mathcal {I}^{\prime }(t_{i}.\text {source})=\top \). Moreover, we know that \(s^{\prime }.\texttt {out\_trs}{}=\varnothing \) by Lemma 1(5).

  Let \(\mathcal {I}_{0}\) be the interpretation that maps \(\{s^{\prime },t_{1},\ldots ,t_{m}\}\) in ⊥ and behaves as \(\mathcal {I}^{\prime }\) on all other arguments. For all transitions t_i, we have that \(\mathcal {I}_{0}\models {} \texttt {end}(t_{i}.\texttt {source})\) holds, because by Lemma 1(3) there is at most a selected transition outgoing from t_i.source in \(\mathcal {I}^{\prime }\) and we deselected it. Moreover, \(\mathcal {I}_{0}\models {} \texttt {fts.fm}\), \(\mathcal {I}_{0}\models {} \phi _{\texttt {initial}}\), \(\mathcal {I}_{0}\models {} \phi _{\texttt {inner}} \), and \(\mathcal {I}_{0}\models {} \phi _{\text {single}} \) hold. Therefore \(\mathcal {I}_{0}\models {} \texttt {is\_useful\_state}(t_{i}.\texttt {source})\) holds.

  By induction we have that there are a configuration \(\lambda _{\mathcal {I}_{0}} \in {\Lambda }\) and a selected initial path P₀ of \(\mathcal {F}|_{{\lambda _{\mathcal {I}_{0}}}}\) that reaches t₁.source and (together with \(\mathcal {I}_{0}\)) satisfies conditions (1) and (2). Clearly, \(\lambda _{\mathcal {I}_{0}}=\lambda _{\mathcal {I}^{\prime }}\) (by construction of \(\mathcal {I}_{0}\)). Extending P₀ with the transition t₁ and the state \(s^{\prime }\), we obtain an initial path \(\mathsf {P}^{\prime }\) that reaches \(s^{\prime }\) and (together with \(\mathcal {I}^{\prime }\)) satisfies conditions (1) and (2).

□

Finally, the following theorem formally states the correctness of the formulas exists_deadlock(s), is_not_dead_transition(t), and may_be_opt_transition(t).

Theorem 1 (correctness of the formulas for checking the behavioural ambiguities)

Let fts be the global data structure representing the FTS \(\mathcal {F} = (S,{{{{\varSigma }}}},s_{0},\delta ,F,{\Lambda })\) and let s be a state of \(\mathcal {F}\). Then

1. 1.

   The formula exists_deadlock(s) is satisfiable iff there is a configuration λ ∈Λ such that the state s is a deadlock in \(\mathcal {F}|_{\lambda }\).

2. 2.

   The formula is_not_dead_transition(t) is satisfiable iff there is a configuration λ ∈Λ such that the LTS transition corresponding to transition t is reachable in \(\mathcal {F}|_{\lambda }\).

3. 3.

   The formula may_be_opt_transition(t) is satisfiable iff there is a configuration λ ∈Λ such that the state t.source is reachable in \(\mathcal {F}|_{\lambda }\) and the LTS transition corresponding to transition t is not reachable in \(\mathcal {F}|_{\lambda }\).

Proof

Straightforward from Lemma 2. □

5.3 Algorithms

The algorithm in Listing 1 below uses the function check to verify whether a propositional formula ϕ is satisfiable, namely to verify the existence of an interpretation (an assignment of truth values to propositions in \(\mathbb {B}(F\cup S\cup T)\)) that makes the formula valid. This is the core functionality of all SAT solvers.

Ambiguities discovery algorithm

Full size image

Theorem 2 (correctness of the ambiguities discovery algorithm)

Let fts be a data structure representing an FTS. The execution of the algorithm in Listing 1 terminates and at the end of the execution the following holds.

1. 1.

   For each state s,

   if s is a hidden deadlock, then s.hdead = True; otherwise s.hdead = False.

2. 2.

   For each transition t,

   1. (a)

      if t is dead, then t.dead = True; otherwise t.dead = False;

   2. (b)

      if t is false optional, then t.false_opt = True; otherwise t.false_opt = False.

Proof

Correctness of the formulas exists_deadlock(s), is_not_dead_transition(t), and may_be_opt_transition(t) is stated by Theorem 1.

The algorithm first detects all the hidden deadlocks (lines 3–7, where the test in line 4 detects the states that are deadlocks in the FTS), thus establishing the invariant in lines 9–10.

Then it detects all the dead transitions and all the false optional transitions (lines 12–18, where the test in line 15 detects the dead transitions that cannot be false optional because they are dead or labelled with ⊤), thus establishing the invariant in lines 20–21 while keeping the invariant in lines 9–10 (since the Boolean flags hdead of the states are not modified).

The termination of the algorithm is straightforward since the number of states and transitions of the FTS is finite. □

It is worth observing that, whenever one is only interested in detecting the hidden deadlocks, it is enough to run only the first part (lines 1–10) of the algorithm in Listing 1: this part represents a specialised algorithm that only detects hidden deadlocks.

Remark 1 (The FTS ambiguity detection problem is NP-complete)

For every propositional formula ϕ with variables in F, the FTS

is such that its (unique) transition is: (i) dead if and only if ϕ is not satisfiable (i.e. ¬ϕ is valid); and (ii) false optional if and only if ¬ϕ is not satisfiable (i.e. ϕ is valid). Moreover, state s₀ is a hidden deadlock if and only if ϕ is not satisfiable. Thus, the FTS ambiguity detection problem is NP-hard. Moreover, the algorithm in Listing 1 can be transformed into an algorithm that, given the data structure fts (cf. Section 5.1) representing an FTS \(\mathcal {F}\) with n states and m transitions, reduces (in polynomial time in the size of fts) the ambiguity detection problem for \(\mathcal {F}\) to n + 2 × m SAT problems (each problem consisting of a formula whose size is linear in the size of fts), as follows:

• extend the data structure introduced in Section 5.1 by adding a field hdead_formula to each state and by adding a field dead_formula and a field false_optional_formula to each transition;

• replace line 7 by s.hdead_formula := exist_deadlock(s);

• replace line 14 by t.dead_formula := is_not_dead_transition(s); and

• replace lines 15–18 by t.false_opt_formula := may_be_opt_transition(s).

Solving the SAT problems stored in the fields hdead_formula, dead_formula, and false_optional_formula provides a solution to the ambiguity detection problem for the given FTS, therefore we conclude that the FTS ambiguity detection problem is NP-complete.

In this section, we apply the new algorithm to a number of exemplary FTSs from the literature. The python code of the implementation and all FTS models allowing the verification of the examples presented in this section are publicly available (ter Beek et al. 2019c). We first discuss the experiments (in Section 6.1) and then the corresponding performance results (in Section 6.2).

6.1 Experiments

Vending Machine

In Fig. 8, we depict the FTS modelling the behaviour of a configurable vending machine from Classen (2011), an FTS benchmark which was used in ter Beek et al. (2019a) and in many other publications (Classen et al. 2010, 2013; Devroey et al. 2014b, 2016b; ter Beek et al. 2015a, 2015b, 2019b; Dimovski et al. 2017; Dimovski and Węsowski 2017; Castro et al. 2018; Dimovski 2018, 2020; Dubslaff 2019). It serves a beverage (soda or tea) either for free or upon payment, in which case a compartment is opened for the customer to take the beverage after which it closes again. Its feature model is represented by the formula s ∨ t over the 4 features {f, c, s, t}, thus resulting in 12 product configurations (viz. 2⁴ − 4, excluding the product configurations \(\varnothing \), {f}, {c}, and {f, c} that lack both features s for soda and t for tea). The FTS of the vending machine contains only 9 states and 13 transitions.

FTS of the vending machine from Classen (2011)

Full size image

Listing 2 reports the result of applying our static analysis algorithm to this FTS. The FTS contains no dead transitions and no hidden deadlocks, but it does contain the 6 false optional transitions (2,change,¬f,3), (4,return, c,1), (5,serveSoda, s,7), (6,serveTea, t,7), (8,take,¬f,9), and (9,close,¬f,1). Thus, the FTS is ambiguous, but it would suffice to turn its false optional transitions into must transitions to make the FTS unambiguous.

Coffee Machine

In Fig. 9, we depict the FTS modelling the behaviour of a configurable coffee machine family from Belder et al. (2015). Originally introduced in Fantechi and Gnesi (2008), this is another SPL benchmark which was already used in ter Beek et al. (2019a) and in a number of other publications (Asirelli et al. 2010, 2011; ter Beek et al. 2012, 2013, 2015c, 2016a, 2016b; ter Beek and de Vink 2014a, 2014b; Beohar et al. 2016, 2018).^{Footnote 4} The coffee machine serves a (possibly sugared) beverage (coffee, tea, or cappuccino) upon the insertion of a coin (euro or dollar), after which the customer takes her/his beverage (possibly following a ringtone). Its feature model is represented by the formula \(\textsc {fm}_{\textsc {c}} = M\wedge W\wedge C\wedge (E\oplus D)\wedge (P\rightarrow R)\wedge (\neg (P\wedge D))\) over the features F_c = {M, W, C, E, D, P, R, T, X}, resulting in 12 product configurations which accept either euros or dollars and offer coffee (with sugar) and possibly tea and cappuccino (upon a ringtone and only for euros). The FTS of the coffee machine contains 14 states and 23 transitions.

FTS of the coffee machine from Belder et al. (2015)

Full size image

Listing 3 reports the result of applying our static analysis algorithm to this FTS. The FTS contains no dead transitions and no hidden deadlocks, but it contains 14 false optional transitions such as (1,sugar, W,2), (1,no sugar, W,3), (2,coffee, C,6), (8,pour tea, T,12), and (13,take cup, M,0). Thus, the FTS is ambiguous, but it would suffice to turn its false optional transitions into must transitions to make the FTS unambiguous.

Coffee/Soup Machine

In Belder et al. (2015), this family of coffee machines was extended with an optional soup component running in parallel with the beverage component. The FTS modelling the behaviour of this soup component is depicted in Fig. 10.^{Footnote 5} The resulting family of vending machines is such that each product allows the insertion of either euros or dollars (returned upon a cancel) in one of its components. The customer chooses a beverage or, if available, a type of soup (at least one among chicken, tomato, pea), which requires to place a cup. A cup detector is optional (mandatory for dollars). Whenever present, soup is only poured if a cup was placed. Placing a cup may need to be repeated if not detected. A choice for soup may be cancelled until a cup is detected. Optionally, a ringtone may ring upon delivery (mandatory for cappuccino, as before), after which the customer takes her/his cup (with a drink or soup) and can again insert a coin in one of the components. The feature model of the soup component is represented by the formula fm_c ∧fm_s ∧SC, where \(\textsc {fm}_{\textsc {s}} = (U\rightarrow \textit {SC})\wedge (S\leftrightarrow \textit {SC})\wedge (\textit {CS}\vee \textit {PS}\vee \textit {TS}\vee \neg S)\wedge ((D\wedge \textit {SC})\rightarrow U)\), over the features F_c ∪{SC, U, S, CS, PS, TS}. The FTS of the soup component contains 13 states and 28 transitions.

FTS of the soup component from Belder et al. (2015)

Full size image

Result of the static analysis on the FTS of Fig. 8

Full size image

Result of the static analysis on the FTS of Fig. 9

Full size image

Listing 4 reports the result of applying our static analysis algorithm to this FTS. The FTS contains no hidden deadlocks and no dead transitions, but it contains the 7 false optional transitions (3,place cup, U,2), (5,place cup, U,4), (7,place cup, U,6), (8,pour tomato, TS,11), (9,pour chicken, CS,11), (10,pour pea, PS,11), and (12,take soup, M,0). Thus, the FTS is ambiguous, but it would suffice to turn its false optional transitions into must transitions to make the FTS unambiguous.

Result of the static analysis on the FTS of Fig. 10

Full size image

The feature model of the composite FTS that results from running the (optional) soup component depicted in Fig. 10 in parallel with the beverage component of the FTS of the coffee machine depicted in Fig. 9 is represented by the formula fm_c ∧fm_s over the features F_c ∪{SC, U, S, CS, PS, TS}, giving rise to 244 product configurations.^{Footnote 6} The composite FTS contains 182 states and 691 transitions.

Listing 5 reports the result of applying our static analysis algorithm to this composite FTS. The composite FTS contains no hidden deadlocks, 284 false optional transitions and 8 dead transitions. The false optional transitions are obviously due to the relatively large amount of false optional transitions in the two component FTSs. The dead transitions can be explained by analysing the execution traces. Consider, for instance, the dead transition (12,insertSoupDollar, SC ∧ D,29). Its source state can be reached upon inserting a coin, followed by choosing sugar and ordering cappuccino, which we recall to require feature P. If the inserted coin was a euro, requiring feature E, then the transition cannot be executed since features E and D exclude each other, while if the inserted coin was a dollar, requiring feature D, then the transition cannot be executed since P and D exclude each other. Since any product has either D or E, indeed in all product LTSs this transition is not reachable. A similar reasoning applies to the skip transitions, which require a feature R that cannot be part of product LTSs in which their sources states are reachable. Hence, the FTS is ambiguous, but it would suffice to remove its dead transitions and turn its false optional transitions into must transitions to make the FTS unambiguous.

Result of the static analysis on the composite FTS resulting from the parallel composition of the beverage component of the FTS of the coffee machine depicted in Fig. 9 and the soup component depicted in Fig. 10

Full size image

Since neither the beverage component nor the soup component has any dead transitions, this shows that the parallel composition of FTSs (with some features in common) without dead transitions may result in a composite FTS with dead transitions. Furthermore, the size of the composite FTS is such that analysis by hand is infeasible. In the remainder of this section, we consider even larger examples to illustrate the scalability of our approach.

Mine Pump

In Fig. 11, we depict the FTS modelling the behaviour of the system FTS modelling the logic of a configurable controller of the mine pump model from Classen(2010, 2011), a standard SPL benchmark for FTSs which was used in ter Beek et al. (2019a) and in many other publications (Classen et al. 2010, 2012, 2013; Cordy et al. 2012, 2013b; Dimovski et al. 2015, 2017; Devroey et al. 2016b; ter Beek et al. 2017, 2020b; Dimovski and Węsowski 2017). The controller of this mine pump model is the parallel composition of the system FTS with the state FTS, depicted in Fig. 12. The mine pump has to keep a mine safe from flooding by pumping water from a shaft while avoiding a methane explosion.

The system FTS of the mine pump model from Classen (2011) (we have labelled transitions that were unlabelled with τ|⊤)

Full size image

The state FTS of the mine pump model from Classen (2011)

Full size image

Therefore, the controller interacts with an environment: it operates a water pump based on water and methane level sensors, modelled by three further FTSs. The parallel composition of these five FTSs constitutes the complete mine pump model. We depict the FTS of the methane level in Fig. 13 and refer to Classen (2010, 2011) for the remaining FTSs. The feature model of the mine pump model can be represented by the formula \(\phi = (c\!\leftrightarrow \!(\textit {ct}\vee \!\textit {cp}))\wedge l\) over the feature set F = {c, ct, cp, m, l, ll, ln, lh}, thus resulting in 64 products (viz. 2⁶, since ϕ is equivalent to considering features {ct, cp, m, ll, ln, lh} to be optional). The system FTS of the mine pump model contains 25 states and 41 transitions.^{Footnote 7} The controller of the mine pump model, composed of the system and state FTSs, contains 77 states and 104 transitions. The complete mine pump model, composed of five FTSs, contains 418 states and 1,255 transitions.

FTS of the methane level environment from Classen (2011)

Full size image

Listing 6 reports the result of applying our static analysis algorithm to the system FTS. The FTS contains no dead transitions, but 25 false optional transitions, among which (s₇,levelMsg, l, s₂₀), and one hidden deadlock state, viz. s₂₀. Indeed, state s₂₀ is reachable in all products upon the execution of two must transitions (the second one being the false optional transition (s₇,levelMsg, l, s₂₀)), while s₂₀ is a deadlock in all 8 products that lack any of the features from the subset {ll, ln, lh}.

Result of the static analysis on the FTS of Fig. 11

Full size image

Hence the system FTS is ambiguous, but it would suffice to turn its false optional transitions into must transitions and to add an explicit deadlock state s_‡ and a transition (s₂₀,‡,¬ll ∧¬ln ∧¬lh, s_‡) to make the system FTS unambiguous.

Actually, a deadlock often indicates an error in the modelling, either in the feature model or in the behavioural model, i.e., the FTS. In fact, another solution to make the system FTS unambiguous would be to slightly change the feature model, e.g., by requiring the presence of at least one of the features ll, ln, or lh via an or-relationship. Doing so, the feature model becomes \(\phi = (c\leftrightarrow (\textit {ct}\vee \!\textit {cp}))\wedge l\wedge (\textit {ll}\vee \!\textit {ln}\vee \!\textit {lh})\), thus resulting in 56 products (i.e., excluding the 8 products over F that satisfy \((c\leftrightarrow (\textit {ct}\vee \!\textit {cp}))\wedge l\), but lack any of the features from the subset {ll, ln, lh}). In Classen (2010, 2011), and Classen et al. (2010), instead, an alternative feature model in which only c (and implicitly ct and cp) and m are optional was considered, resulting in only the four products over F that satisfy \((c\leftrightarrow (\textit {ct} \wedge \textit {cp}))\wedge l\wedge \textit {ll}\wedge \textit {ln}\wedge \textit {lh}\).

Yet another solution to make the system FTS unambiguous would be to slightly change the FTS itself, to make sure that it contains neither a hidden nor an explicit deadlock state. In this case, it would suffice to add one or more transitions to leave state s₂₀ in a meaningful way. This is the solution opted for in Classen et al. (2013), Dimovski et al. (2015), Dimovski et al. (2017), ter Beek et al. (2017), and Dimovski and Węsowski (2017), which use the specification in fPromela of the complete mine pump model as originally distributed with SNIP (Classen et al. 2012) and its re-engineered successor ProVeLines (Cordy et al. 2013a) (https://bitbucket.org/maxcordy/provelines-cora/) or their translations for mCRL2 (Cranen et al. 2013; Bunte et al. 2019) (http://www.mcrl2.org/) or VMC (ter Beek et al. 2012; ter Beek and Mazzanti 2014) (http://fmt.isti.cnr.it/vmc/). Basically, three transitions are added to the system FTS of Fig. 11 from state s₂₀ to the initial state s₆ to cover the cases in which features from the subset {ll, ln, lh} are missing, viz. (s₂₀,highLevel,¬lh, s₆), (s₂₀,lowLevel,¬ll, s₆), and (s₂₀,normalLevel,¬ln, s₆).

The false optional transitions and the hidden deadlock state of the system FTS are propagated into the controller of the mine pump model, which we recall to be the parallel composition of the system and state FTSs. Application of our static analysis algorithm to the FTS of the controller of the mine pump model reports that the FTS contains no dead transitions, 59 false optional transitions, and 4 hidden deadlock states. The situation is different for the complete mine pump model, which we recall to be the parallel composition of five FTSs, viz. the system and state FTSs and three further FTSs that model a water pump and water and methane level sensors. From the FTS of the methane level, depicted in Fig. 13, we immediately note that the actions methaneRise and methaneLower are local actions of this FTS that do not synchronise with any of the other four FTSs. Hence, while the solutions suggested above would make the system FTS of Fig. 11 unambiguous, it is clear that the FTS of the complete mine pump model is deadlock-free, since it can indefinitely execute the sequence of actions methaneRise followed by methaneLower. This is confirmed by our static analysis algorithm applied to the FTS of the complete mine pump model, which reports that the FTS contains no dead transitions and no hidden deadlock states, but a stunning 308 false optional transitions.^{Footnote 8} The fact that the system FTS has hidden deadlock states that are no longer present in the FTS of the complete mine pump model demonstrates the usefulness of analysing component FTSs in isolation.

In general, while the parallel composition of unambiguous FTSs does not introduce false optional transitions, the composite FTS may contain dead transitions or hidden deadlock states. We have seen an example of the introduction of dead transitions in the composite FTS of the coffee and soup component, whose individual FTSs did not exhibit dead transitions.

The application of the static analysis algorithm to individual component FTSs is surely desirable as it results in less ambiguous specifications of the components constituting a composed system, and it possibly allows more efficient model checking of the composed system (more on this in the next section, cf. the part of Fig. 4 that is not red). A further advantage is that our approach becomes applicable also to feature-oriented systems composed by superimposition, since in Dubslaff (2019) it is shown how to transform feature-oriented systems composed by parallel composition into feature-oriented systems composed by superimposition while maintaining behaviour and modularity.

Instead, the application of the static analysis algorithm to a composed FTS resulting from the parallel composition of several FTSs is less desirable because the benefits of detecting ambiguities are greatly reduced. This is due to the lack of a detailed specification of the composed FTS, which is merely a semantic model without a matching syntactic specification. Note that composed configurable systems can also be described as Multi SPLs (MPLs), i.e., sets of interdependent SPLs (Holl et al. 2012). It is not clear how to obtain results for composed FTSs by reusing results of analyses performed in isolation on its component FTSs, in analogy with recently proposed compositional approaches for analysing MPLs (Lienhardt et al. 2018a; Damiani et al. 2019).

Claroline

We conclude this section with a very large (monolithic) system. The Claroline SPL is a configurable system whose FTS model, originally introduced in Devroey et al. (2014a), was reverse-engineered from an Apache weblog (containing 12,689,030 HTTP requests) of a dynamically configurable course platform used at the University of Namur. The FTS model has since been used in several publications (Devroey et al. 2014c, 2015, 2016a, 2016b, 2017, 2018). The Claroline SPL has 44 features and its feature model is quite large: it is represented by a formula with 299 logical connectives (omitted here), resulting in more than 5,000,000 product configurations. The FTS of Claroline contains 107 states and 11,236 transitions. Application of our static analysis algorithm reports (after running for about one hour) that the FTS contains no dead transitions and no hidden deadlock states, but 259 false optional transitions. Note that, since the FTS of Claroline has been generated from the analysis of actual execution paths, the discovery of dead transitions would have immediately signalled some major bug either in the feature model or in the feature expressions, or in the log analysis procedure.

6.2 Performance results

In Table 1, we report some data concerning the static analyses of the FTSs discussed above.

The FTSs of the vending machine, the coffee machine, and the soup component are all live (i.e., no deadlocks), with no dead transitions, while a respective 46%, 61%, and 25% of their transitions are false optional. Their static analyses are immediate. Also the FTS of the coffee/soup machine is live, but 41% and 1% of its transitions are false optional and dead, respectively. Its static analysis takes about a minute. The static analysis of the system FTS of the mine pump and that of the mine pump controller (i.e., the parallel composition of the system FTS and the state FTS) are immediate, but neither of these FTSs is live because 4% and 5% of their states, respectively, are hidden deadlocks. None of their transitions are dead, but 61% and 57% are false optional, respectively. Instead, the FTS of the complete mine pump is live and it has no dead transitions, but 25% of its transitions are false optional. Its analysis is not immediate, but takes a few minutes. Recall that this analysis could not be performed in a reasonable amount of time with the static analysis algorithm from ter Beek et al. (2019a). The FTS of Claroline, finally, requires about an hour to analyse. It is live and it has no dead transitions, but 2% of its transitions are false optional.

Next, we compare the current implementation of the static analysis algorithm, as introduced in Listing 1, with the implementation used in ter Beek et al. (2019a), where an algorithm looks for all simple paths from the initial state to each state by visiting all cycle-free paths (starting from the initial state) in a depth-first manner. The results are reported in Table 2, where timeout stands for ‘aborted after more than 2 hours’. The results show a clear improvement in runtime, ranging from a 3.54x speedup for the FTS of the vending machine to speedups of > 7200x for the three largest FTSs. This demonstrates the improved efficiency of the current implementation.

In Table 3, we report a comparison of the current implementation of the static analysis algorithm with a specialised implementation that only detects hidden deadlocks, applied to the three largest FTSs showcased in this section. This specialised implementation refers to the first part (lines 1–10) of the static analysis algorithm in Listing 1, which (as pointed out at the end of Section 5) represents a hidden deadlocks discovery algorithm (i.e., analysing only liveness). The results show that only a fraction of the runtime of the current implementation is needed for deadlock detection, ranging from 6.06% for the FTS of the coffee/soup machine to only 2.97% and 3.59% for the complete mine pump and Claroline FTSs, respectively.

All the experiments presented in this section were performed on a Mac Pro (Late 2013) 3.7 Ghz Quad-Core with an Intel Xeon E5 processor with 10 Mb L3 cache and 64 Gb (four 16 Gb) of 1866 Mhz DDR3 ECC memory. All the experiments were performed five times each and the average time and memory usage of each was collected and reported in the tables. We used Python 3.6.

In analogy with anomaly detection in feature models, dead featured transitions in an FTS clearly indicate a modelling error, whereas false optional featured transitions often provide a wrong idea of the domain by giving the impression that certain behaviour is optional while actually it is mandatory (i.e., it occurs in all products of the FTS). However, our engineering methodology (i.e., the top-right red part of Fig. 4) that allows the transformation of an ambiguous FTS into an unambiguous FTS also serves another purpose, viz. to facilitate a kind of family-based model checking of properties expressed as logic formulas. As anticipated in earlier sections, according to the strategy outlined in Fig. 4 (the part that is not red), a property ϕ specified in either LTL or v-ACTLive\(^{\Box }\) can be verified (with a linear complexity) directly on an unambiguous FTS \(\mathcal {F}\) (ignoring its feature expressions) such that ϕ holds for all product LTSs in \(\mathsf {lts}(\mathcal {F})\) whenever it holds for \(\mathcal {F}\). This strategy offering a number of efficient verification options is another contribution of this paper.

An FTS that has no hidden deadlocks is said to be live. In this section, we show that a live FTS enjoys the property that all valid linear-time LTL formulas are preserved by all its products, as well as all valid branching-time v-ACTLive\(^{ \Box }\) properties (as we already showed in ter Beek et al. (2019a)). Intuitively, these results are based on the fact that all transitions (and thus paths) in products of an FTS \({\mathcal {F}}\), i.e. LTSs in \(\mathsf {lts}(\mathcal {F})\), also occur in \({\mathcal {F}}\).

Branching-time Properties

To start with the latter, v-ACTLive\(^{ \Box }\) is a rich fragment of the variability-aware action-based and state-based branching-time modal temporal logic v-ACTL and it is interpreted on so-called ‘live’ MTSs (ter Beek et al. 2015a, 2015b, 2016a, 2019d). A Modal Transition System (MTS) is an LTS that distinguishes admissible (‘may’), necessary (‘must’), and optional (may but not must) transitions such that by definition all necessary and optional transitions are also admissible (Larsen and Thomsen 1988; Křetínský 2017). In ter Beek et al. (2016a), an MTS is defined to be live if all its states are live, where a live state of an MTS is such that it does not occur as a final state in any of its products (these are LTSs obtained from the MTS in a way similar to Definition 4), resulting in an MTS in which every path is infinite. Then it is proved that the validity of formulas expressed in v-ACTLive\(^{ \Box }\) is preserved in all products (cf. ter Beek et al. 2016a, Theorem 4), thus allowing a kind of family-based model checking of MTSs. It is not difficult to see that this result continues to hold for MTSs whose every state is either live or final.

Note that any FTS \({\mathcal {F}}\) can be transformed into an MTS \({\mathcal {F}}_{\text {MTS}}\) by considering its must transitions as necessary transitions, its featured transitions as optional transitions, and all its transitions as admissible, and by removing all feature expressions. If \({\mathcal {F}}\) is live, then \({\mathcal {F}}_{\text {MTS}}\) is live, with respect to the FTS’s set of products \(\mathsf {lts}(\mathcal {F})\), because it has no hidden deadlocks.^{Footnote 9}

Moreover, all transitions of \({\mathcal {F}}\) whose corresponding (LTS) transitions are mandatorily present in all products correspond to necessary transitions in \({\mathcal {F}}_{\text {MTS}}\). This demonstrates that the above mentioned result from ter Beek et al. (2016a) can be carried over to live FTSs, thus allowing a kind of family-based model checking of such FTSs for the v-ACTL fragment v-ACTLive\(^{\Box }\). Hence, the following result holds, where ⊧ denotes the satisfaction relation of v-ACTLive\(^{\Box }\) interpreted over MTSs.

Proposition 1

(ter Beek et al. 2019a) Any formula ϕ of v-ACTLive\(^{ \Box }\) is preserved by live FTSs: given a live FTS \({\mathcal {F}}\), whenever \({\mathcal {F}}_{\text {MTS}}\models \phi \), then \({\mathcal {F}}|_{\lambda }\models \phi \) for all products \({\mathcal {F}}|_{\lambda }\in \mathsf {lts}(\mathcal {F})\).

Furthermore, note that states in an FTS that are the source of at least one must transition are by definition live. Hence, replacing all redundant feature expressions of false optional transitions (syntactic sugar) with ⊤ results in more must transitions, thus allowing for a more efficient kind of (family-based) verification.

Linear-time Properties

In addition to ter Beek et al. (2019a), here we also consider linear-time properties. As said before, a live FTS also enjoys the property that all valid linear-time LTL formulas are preserved by all its products. This can be seen as follows.

A path in an LTS is said to be maximal if it cannot be extended further, i.e. it is infinite or it ends in a deadlock state.

Model checking LTL formulas on an LTS reduces to analysing its maximal paths: an LTL formula is valid if it holds for all maximal paths. These notions trivially carry over to FTSs by ignoring their feature expressions. Clearly, if an FTS is live, i.e. it has no hidden deadlocks, then the set of maximal paths of any product (LTS) is a subset of the set of maximal paths of the FTS.

Hence, the following result holds, where \({\mathcal {F}}_{\text {LTS}}\) denotes the LTS obtained from an FTS \(\mathcal {F}\) by removing its feature expressions and ⊧ denotes the satisfaction relation of LTL interpreted over LTSs.

Proposition 2

Any formula ϕ of LTL is preserved by live FTSs: given a live FTS \({\mathcal {F}}\), whenever \({\mathcal {F}}_{\text {LTS}}\models \phi \), then \({\mathcal {F}}|_{\lambda }\models \phi \) for all products \({\mathcal {F}}|_{\lambda }\in \mathsf {lts}(\mathcal {F})\).

The results presented in Propositions 1 and 2 show specific cases in which verification of live FTSs reduces to verification (with a linear complexity) of corresponding MTSs and LTSs that are obtained straightforwardly by ignoring the feature expressions (and distinguishing necessary and optional transitions in MTSs). This is made possible by the engineering methodology sketched in Fig. 4 (the top-right red part). However, as illustrated by the strategy outlined in Fig. 4 (the part that is not red), if either the property under verification is not an LTL or v-ACTLive\(^{\Box }\) formula or the result of the verification is false, then the formula needs to be verified with classical (family-based) model checking.

In the remainder of this section, we apply these results to example FTSs from Section 6 and provide examples of v-ACTLive\(^{\Box }\) and LTL formulas to illustrate their impact. The models allowing the verification of the example properties presented in this section are publicly available (ter Beek et al. 2019c).

It is worth noticing that if we are interested in just the liveness of FTSs (e.g. to enable family-based model checking of invariant properties), then the first part (lines 1–10) of the static analysis algorithm in Listing 1 allows to establish the liveness of FTSs in a much more efficient way (cf. Table 3). Recall that this part represents a hidden deadlocks discovery algorithm, which we referred to as the specialised implementation in Section 6.

Vending Machine

We have seen in Section 4.2 how to transform an ambiguous FTS into an unambiguous one. Furthermore, we have seen above how to transform an FTS into an MTS. In Fig. 14, we depict the MTS ^{Footnote 10} that is obtained in this way from the unambiguous (and thus live) FTS (described in the beginning of Section 6) that corresponds to the FTS of Fig. 8.

MTS obtained from the FTS of Fig. 8

Full size image

As we argued in the beginning of this section, the resulting MTS is live, with respect to the FTS’s set of products, thus allowing family-based model checking for v-ACTLive\(^{\Box }\) (cf. Proposition 1). In fact, v-ACTLive\(^{\Box }\) formulas can efficiently be verified on MTSs with the variability model checker VMC (http://fmt.isti.cnr.it/vmc), which is a tool for the analysis of branching-time properties over behavioural SPL models specified as an MTS with a set of logical variability constraints (akin to feature expressions) (ter Beek et al. 2012; ter Beek and Mazzanti 2014).

Originally, VMC used the variability constraints associated with the MTS to dynamically evaluate the liveness of each node. Based on ter Beek et al. (2019a), where we showed how to establish a priori the liveness of all nodes of an FTS, and thus of the MTS that can be obtained by transformation, the most recent prototypical extension of VMC, version 6.5, offers users the possibility to state explicitly that an MTS is live.

The input language of VMC is a process algebra. Listing 7 contains the specification of the vending machine in the process-algebraic input language accepted by VMC. Note that the system part or process model (i.e. without the constraints) can be seen as the natural encoding of the graph (MTS) of Fig. 14, with the process terms corresponding to the states of the graph and SYS indicating the initial state. Intuitively, a.P models a process that executes action a and then behaves as P, while P + Q models a process that non-deterministically chooses to behave as either P or Q. Information on the modality of the transitions (may, must) is defined as a special additional parameter associated to the basic actions of the algebra, the default being must. Finally, Constraints { LIVE } explicitly declares that the MTS is live, the novel feature of VMC v6.5.

Specification in VMC of MTS of Fig. 8

Full size image

Example formulas of branching-time properties of the vending machine that we verified in a kind of family-based manner with VMC include the following:

1. 1.

   AG AF_pay∨free⊤: infinitely often, either action pay or action free is executed;

2. 2.

   AG [open] AF_close⊤: it is always the case that the execution of action open is eventually followed by that of action close;

3. 3.

   AG AF_{cancel∨serveSoda∨serveTea}⊤: infinitely often, either action cancel or action serveSoda or action serveTea is executed;

4. 4.

   ¬E [⊤ _¬teaU_serveTea⊤]: it is not possible that action serveTea is executed without being preceded by an execution of action tea;

5. 5.

   [pay] AF_{take∨cancel}⊤: whenever action pay is executed, eventually also either action take or action cancel is executed.^{Footnote 11}

Obviously, there are also numerous formulas of linear-time properties of the vending machine that can be verified in such kind of family-based manner, with tools such as SPIN (http://spinroot.com/). Example formulas include the following:^{Footnote 12}

1. 1.

   \(\Box (\textit {selected} \Rightarrow \Diamond \textit {served})\): after selecting a beverage, the machine will always eventually serve a beverage;

2. 2.

   \(\Box (\textit {served} \Rightarrow \Diamond \textit {taken})\): after a beverage is served, the customer will always eventually take the beverage.

VMC v6.5 has thus been tailored for family-based model checking of temporal logic properties on FTSs (via their transformation in MTSs). At present, efficient SPL model checking on FTSs can be achieved by using dedicated family-based model checkers such as the ProVeLines (Cordy et al. 2013a) tool suite (including its predecessor SNIP (Classen et al. 2012)) or fNuSMV (Classen et al. 2014), or, alternatively, by using one of the highly optimised off-the-shelf model checkers like SPIN or mCRL2, which have recently been made amenable to family-based SPL model checking on FTSs (Dimovski et al. 2015, 2017; ter Beek et al. 2017, 2020b; Dimovski and Węsowski 2017).

Mine Pump

We have seen in Section 6 that the complete mine pump model (an FTS with 418 states and 1,255 transitions) is live, thus allowing a kind of family-based model checking for v-ACTLive\(^{\Box }\) and LTL (cf. Propositions 1 and 2). In fact, we have done so for the complete mine pump model specification in fPromela, as distributed with SNIP and ProVeLines, and its translation for VMC (recall that the model specifications are publicly available (ter Beek et al. 2019c)).

Example formulas of branching-time properties of the complete mine pump that we verified in such kind of family-based manner with VMC include the following:^{Footnote 13}

1. 1.

   max \(X: (\textit {EX}^{\Box }_{\textit {methaneRise}\vee \textit {methaneLower}}~X)\): the system behaviour includes a (mandatory) path that contains only variations of the methane level;

2. 2.

   AG [palarmMsg] ¬E [⊤ _{¬setMethaneStop}U_palarmMsg⊤]: it is not possible that two palarmMsg actions occur without a setMethaneStop in between;

3. 3.

   AG [highLevel] ¬E [⊤ _¬pumpStartU_lowLevel⊤]: it is not possible that the water level decreases if the pump did not start;

4. 4.

   AG ¬(pumpoff ∧EX_pumpStop⊤): a pumpStop action cannot occur if the pump is already off;

5. 5.

   AG ¬(¬ready ∧EX_pumpStart⊤): a pumpStart action cannot occur if the system is not ready;

6. 6.

   AG [stopCmd] ¬E [¬stopped U_startCmd⊤]: a start command cannot follow a stop command if in the meantime the system did not stop.

Example formulas of linear-time properties of the complete mine pump model that we verified in such kind of family-based manner with SPIN include the following:^{Footnote 14}

1. 1.

   \(\Box (\neg \textit {pumpOn} \vee \textit {stateRunning})\): if the pump is on, the actual pump state is set to running;

2. 2.

   \(((\Box \Diamond \textit {readCommand} ) \wedge (\Box \Diamond \textit {readAlarm} ) \wedge (\Box \Diamond \textit {readLevel} ) ) \Rightarrow (\neg \Diamond \Box (\neg \) pumpOn ∧¬methane ∧highWater)): if the controller can fairly receive each of the three message types, then the pump is never indefinitely off when the water is high;

3. 3.

   \(\Box ((\neg \textit {pumpOn} \wedge \textit {lowWater} \wedge \Diamond \textit {highWater})\Rightarrow ((\neg \textit {pumpOn}) ~U~\textit {highWater}))\): when the pump is off and the water is low, it will only start once the water is high again.

These are precisely the properties #18, #34, and #41, respectively, as verified with both SNIP and SPIN in Classen et al. (2013).

Toolchain

In ter Beek et al. (2021), we present FTS4VMC, a tool developed specifically as a front-end for VMC with a user-friendly GUI. The resulting toolchain allows a modeller to analyse an FTS for ambiguities, remove them, transform the resulting live FTS into an MTS and perform an efficient kind of family-based model checking of v-ACTLive\(^{\Box }\) properties. The FTS4VMC implementation is publicly available from https://github.com/fts4vmc/FTS4VMC.

In this paper, we have revisited several types of static analysis that can be performed over an FTS as part of an engineering methodology. Concretely, we analyse FTSs for hidden deadlocks and anomalies in the form of false optional and dead transitions. The removal of hidden deadlocks improves the clarity of FTSs and enables an efficient kind of family-based model checking of live FTSs. Dead transitions identify real modelling errors present in FTSs that should be removed. False optional transitions reveal redundancies in the feature expressions labelling the FTSs. Moreover, replacing such syntactic sugar by ⊤ leads to more must transitions, which eases verification and may increase the set of properties verifiable by v-ACTLive\(^{\Box }\). We have presented a new algorithm for these static analyses of FTSs, for which we have proved the correctness. We have evaluated the suitability of the new algorithm by applying it to a large number of exemplary FTSs from the literature, and we have also showed the usefulness for an efficient kind of family-based model checking of FTSs. In particular, we have empirically demonstrated the superiority of the new algorithm with respect to the algorithm presented in ter Beek et al. (2019a), by making feasible (in reasonable time) the static analysis of FTSs of considerable size (cf. Table 2).

The python code implementing the algorithm and the specifications of all the models that are needed to reproduce the experiments presented in Sections 6 (static analysis) and 7 (verification) are publicly available (ter Beek et al. 2019c). Also the implementation of the FTS4VMC tool developed specifically as a front-end for VMC is publicly available (cf. Section 7). A front-end tool for SPIN, based on a transformation from FTSs to PROMELA, is ongoing work.

In principle, our static analysis checks could all be performed by classical family-based model-checking approaches by expressing the ambiguity properties in CTL (exploiting the fact that they concern reachability questions). However, verifying such properties for each state and transition of an FTS requires a considerable number of verifications. Moreover, the complexity of verifying a single CTL formula on an FTS is exponential in the number of features (Classen et al. 2014). Note that the kind of family-based model checking we make possible is linear in the size of the LTS or MTS that is obtained from a live FTS (by ignoring its feature expressions). Nevertheless, we intend to investigate this issue in more detail, also empirically, possibly exploiting symbolic representations.

Recently (Lienhardt et al. 2018b), a subset of the authors proposed an approach and a tool for checking SPLs of statecharts (Harel 1987). The tool checks that all the products can be generated and are well-formed statecharts. In future work, we would like to extend it by adding behavioural ambiguity detection analyses like the ones presented in this paper. We also would like to study how to adapt our static analysis algorithms to apply them to high-level SPL modelling languages (e.g. fPROMELA (Classen et al. 2012, 2013) and fNuSMV (Classen et al. 2014)). Finally, it would be interesting to mechanise our formalisations and associated proofs to provide further evidence of the soundness of our static analysis techniques.