=Paper=
{{Paper
|id=Vol-1879/paper56
|storemode=property
|title=A DL Semantics for Reasoning over OVM-based Variability Models
|pdfUrl=https://ceur-ws.org/Vol-1879/paper56.pdf
|volume=Vol-1879
|authors=Germán Braun,Matias Pol'la,Laura Cecchi,Agustina Buccella,Pablo Fillottrani,Alejandra Cechich
|dblpUrl=https://dblp.org/rec/conf/dlog/BraunPCBFC17
}}
==A DL Semantics for Reasoning over OVM-based Variability Models==
https://ceur-ws.org/Vol-1879/paper56.pdf
A DL Semantics for Reasoning over OVM-based
Variability Models
Germán Braun1,3 , Matias Pol’la1,3 , Laura Cecchi1 , Agustina Buccella1,3 , Pablo
Fillottrani2,4 , and Alejandra Cechich1
1
U NIVERSIDAD NACIONAL DEL C OMAHUE 2 U NIVERSIDAD NACIONAL DEL S UR
3
Consejo Nacional de Investigaciones Cientı́ficas y Técnicas (CONICET)
4
Comisión de Investigaciones Cientı́ficas de la Provincia de Buenos Aires (CIC)
Abstract Software Product Line (SPL) development has traditionally included
Variability Management as a way of defining, modelling, implementing and test-
ing variability. In this context, we have created a framework, SeVaTax, based on
extensions of the Orthogonal Variability Model (OVM), and aimed at analysing
properties of variability models and deriving products from an SPL. Despite sev-
eral approaches have proposed techniques for automatically analysing the vari-
ability models’ potential for deriving products, a formalisation of OVM-based
diagrams has not been addressed yet. In this paper, we formally define the syn-
tax and semantics of SeVaTax diagrams expressed in first order logic, introduce
a DL encoding and establish the EXPTIME-membership of reasoning over SeV-
aTax. Based on these results, we are developing a prototype providing a back-end
for the automated support of consistency checks of SeVaTax variability diagrams
along with its encoding into DL knowledge bases.
1 Introduction and Motivation
Variability management [22] is one the most challenging and important activities of
the domain and application engineering phases of an SPL development. During the
domain engineering, variability must be defined, modelled, implemented, and validated
taking into account domain constraints and the flexibility the SPL should provide. Then,
during the application engineering, this variability is instantiated in order to derive new
products from the SPL. These products must consider the application requirements,
which must be validated according to specific combinations of variability constraints
imposed by the model. Particularly, a new research topic has emerged for this validation
as automated variability analysis, which focuses on a set of techniques for translating
and validating variability models by considering the anomalies or mismatches these
models may contain [16, 20, 27, 3]. On this line, checking consistency of variability
models (VM) is still a critical problem. In previous works, we have introduced a process
for implementing variability analysis [5, 6]; and we have defined a framework, SeVaTax
[23], which includes selecting variants according to the needs and characteristics of new
products, and assembling software components for those products.
In the literature, several works propose different techniques and methods for the
analysis process, many of them focused on the analysis of Feature Models (FMs) [14]
or OVMs but using back-end SAT solvers [3, 31, 20, 32, 18, 13, 28, 19]. In this respect,
SAT-based approaches inherit some limitations from more restrictive logics and thus
failing to reflect the finer logical structure of variability models. Particularly, SAT-based
proposals miss the relationships amongst services when embedding variability models
in CNF. As a consequence, the domain validation process involves several product-
by-product SAT checks, i.e. setting CNF input formulae according to each possible
instantiation derived from the selection of services in the domain model. Therefore,
identifying inconsistency sources is hard in such approaches as has also been evaluated
in [23]. Aiming at addressing these drawbacks and improving the variability analysis
process, we consider the well-known benefits of using DL to conceptual representa-
tion in terms of classes and relationships admitting decidable reasoning. Even though
it seems to fit with our requirements, a formalisation of OVM-like diagrams is still
missing and therefore validations in existing approaches are not reliable enough either.
Based on this motivation, in this work we propose the formalisation of SeVaTax
diagrams expressed in first order logic, and introduce an ALCI encoding allowing ex-
tended reasoning capabilities. We also conclude that reasoning on SeVaTax diagrams
is EXPTIME w.r.t. service consistency. From these results, we are developing a proto-
type providing a back-end for the automated support of consistency checks of SeVaTax
variability diagrams along with its encoding into DL knowledge bases.
This work is structured as follows. Section 2 briefly describes the SeVaTax frame-
work, its graphical primitives and a required set of reasoning services to check them.
Section 3 introduces the FOL formalisation of SeVaTax diagrams and section 4 presents
the corresponding ALCI encoding together with complexity results. Finally, section 5
shows some related works and section 6 concludes with the main contributions and
future works.
Figure 1. General Process for Automated Variability Analysis Process
2 The SeVaTax Framework
The automated variability analysis process includes five components, as depicted in Fig.
1. The first component is the variability model, which may be specified by some of the
different modelling languages, such as Feature Model (FM), OVM or Constraint Vari-
ability Language (CVL) [11], among others. The second component is a translator for
transforming the graphical model into a formal representation. The output of this trans-
lator is sent to a reasoner responsible for validating the model. The results of this pro-
cess are defined according to the next most common cases extracted from the literature:
Valid Model (VM), Valid Instantiation (VI), All Products (AP), Instantiation Number
(IN) and Problem Detection (PD). The first one, VM, determines whether is possible to
generate a product from a variability model; VI checks if the instantiation might gener-
ate a valid product given a model and one of its configurations; AP determines all the
possible instantiations; and IN specifies the number of possible instantiations. Finally,
PD is responsible for identifying the causes which determine that a model is invalid.
One of the main components of the SeVaTax framework is the graphical language
based on an OVM-extended notation for representing each SPL functionality. In previ-
ous works [6, 5], we have already defined this model based on a functionality-oriented
methodology. That is, each functionality of the SPL is modelled as a functional data-
sheet represented by a set of services, common1 and variant ones, interacting among
them for performing the functionality. Each datasheet includes a set of hierarchical
structures, where each structure is composed by a root service and a set of services
(variation points or variants). Then, during the derivation process, these variants are
selected configuring a new product and providing flexibility to the SPL.
We have defined a set of interactions that allows us to represent the functional-
ity as graphical notation. These interactions involve common and variant services, and
are divided into variability types for denoting the variant interactions among services;
dependencies for denoting interaction between services; and scope for specifying the
scope of each variant point [4]. The complete set of interactions supported in this work
(and graphically depicted in Fig. 2) are:
Variability Types:
- Mandatory variation point: it determines the selection of a variant service when the
variation point is included in the product being derived.
- Optional variation point: it specifies that zero or more variant services, associated to
the variation point, can be selected.
- Alternative variation point: it defines that only one variant service, of the set of as-
sociated variants of the variation point, must be selected (XOR relation).
- Variant variation point: it defines that at least one variant service, of the set of asso-
ciated variants of the variation point, must be selected (OR relation).
Dependencies:
- Requires: it specifies a relation between two variant services in which the selection of
one variant service requires the selection of the other one.
- Excludes: it is the opposite of the requires dependency specifying the exclusion of a
variant when another one is selected.
Figure 2. Left-Right: Mandatory; Optional; Alternative; Variant; Requires; Excludes. VP = Vari-
ation Point. V = Variant.
1
Common services are services which will be part of every product derived from the SPL
The SeVaTax framework also provides the following primitive and scope operators,
which are out of scope of this work:
- Uses ( ) dependency: it specifies a dependence between common services,
which are not necessarily associated with a variation point.
- Global Variation Point (Global VP) ( ): it specifies that if the variation point is
instantiated in a specific way, it will be applied in that way for all functionality including
that variation point.
- Specific Variation Point (Specific VP)( ): it specifies that the instantiation of the
variation point is particular for each functionality including that variation point.
A SeVaTax model provides a graphical notation depicting associations between two
specific types of services, variation point (VP) and variant (V). In this work, associations
may be variability types and dependencies. Each variability must relate one VP with a
set of at least one V or VP. Moreover, each V must be only associated to one and only
one VP.
Figure 3. Left-Right: Alternative variability type for OS; Mandatory variability type for Con-
nectivity.
Example 1. Fig. 3 depicts alternative and mandatory variability types modelling the
variant of an operating system (OS) and the connectivity for a mobile phone, respect-
ively. The OS variation point allows configuring three possible products: {OS, WinCE},
{OS, Symbian} and {OS, Android}. The Connectivity VP configures only the follow-
ing product: {Connectivity, WIFI, USB, Bluetooth}.
Towards a new implementation of the SeVaTax framework, we present a formalisa-
tion of the OVM-based models and introduce a novel DL encoding to check diagrams
for consistency, which have not been yet combined into the very same framework.
3 Formalising SeVaTax Diagrams
In this section we introduce the semantics of each variability type: Mandatory, Optional,
Alternative and Optional and dependencies: Requires and Excludes, in terms of first
order logic (FOL). We do not deal with either Uses dependency or scope operators. A
FOL encoding is firstly proposed for analysing general properties of models, and easing
comparisons with related approaches. In next section, this semantics is instantiated in
ALCI.
Definition 1. Let Σ be a SeVaTax diagram. We define Σ F OL as the corresponding set
of FOL assertions representing such diagram and constructed as follows. The signature
of the Σ F OL knowledge base includes the followings domain predicates:
– Sv1 , ..., Svm , Svp1 , ..., Svpn are FOL unary predicates for services, Svj for variant
services and Svpi for variation point services,
– MAND, OPT, ALT and VAR are binary relations. However, we formalize such vari-
ability types as r+1-ary predicates denoted as MANDr+1 , OPTr+1 , ALTr+1 and
VARr+1 , respectively. For instance, if x MAND {y1 , ..., yr } is an association defined
in Σ, we characterise it as the FOL r+1-ary predicate: MANDr+1 (x, y1 , ..., yr ).
– Each dependency REQ and EXC corresponds to the FOL binary predicate REQ
and EXC, respectively.
Now, we proceed to formalise Σ as a set of FOL assertions. Firstly, we introduce the
following background assertion imposing that each service may be instantiated by at
most one element. Such formulae must be specified for each variation point and variant
service in Σ. Then, we introduce the domain axioms describing the variability types
and dependencies of SeVaTax.
∃x.Svpk (x) ∧ ¬∃y.(Svpk (y) ∧ x 6= y) ∃x.Svk (x) ∧ ¬∃y.(Svk (y) ∧ x 6= y)
¬∃x.(Svpi (x)∧Svpl (x)), 1 ≤ i, l ≤ n, ¬∃x.(Svj (x)∧Svl (x)), 1 ≤ i, l ≤ m, i 6= l
Mandatory: for each MANDm+1 in the signature of Σ F OL
m
^
∃x.MANDm+1 (x, y1 , ..., ym ) ∧ Svpk (x) → (Svpi (yi ) ∨ Svi (yi )), m ≥ 1
i=1
m
^
∃y1 ...ym .MANDm+1 (x, y1 , ..., ym ) ∧ (Svpi (yi ) ∨ Svi (yi )) → Svpk (x), m ≥ 1
i=1
m
^
∃x, y1 ...ym . MANDm+1 (x, y1 ..., ym ) → x 6= yi , m ≥ 1
i=1
The first and second sentences define the mandatory interaction among services,
which requires that one instance of a variation point is related to each other variant or
variation point through the predicate MANDm+1 , and vice versa. The last one imposes
that the variation point, from which the variability is defined, must not be a variant of
itself.
Optional: for each OPTm+1 in the signature of Σ F OL
∃x. OPTm+1 (x, y1 , ..., ym ) → Svpk (x) , m ≥ 2
m
^
∃x, y1 ...ym . OPTm+1 (x, y1 ..., ym ) → x 6= yi , m ≥ 2
i=1
The first imposes that one instance of a variation point may be related to zero or
more variants or variation points through the predicate OPTm+1 , while the last sen-
tence also imposes that the variation point, from which the variability is defined, must
not be a variant of itself.
Alternative: for each ALTm+1 in the signature of Σ F OL
m
M
∃x.ALTm+1 (x, y1 ..., ym ) ∧ Svpk (x) → (Svpi (yi ) ∨ Svi (yi )), m ≥ 2
i=1
m
M
ALTm+1 (x, y1 ..., ym ) ∧ (Svpi (yi ) ∨ Svi (yi )) → Svpk (x), m ≥ 2
i=1
m
^
∃x, y1 ...ym . ALTm+1 (x, y1 ..., ym ) → x 6= yi , m ≥ 2
i=1
The ⊕ operator is semantically equivalent to the exclusive or (XOR) operation.
Similarly, the first sentence requires that one instance of a variation point is related to
one and only one variant or variation point through the predicate ALTm+1 . The two
last sentences define the same constraints than for the mandatory variability types.
Variant: for each VARm+1 in the signature of Σ F OL
m
_
∃x.VARm+1 (x, y1 ..., ym ) ∧ Svpk (x) → (Svpi (yi ) ∨ Svi (yi )), m ≥ 2
i=1
m
_
VARm+1 (x, y1 ..., ym ) ∧ (Svpi (yi ) ∨ Svi (yi )) → Svpk (x) m ≥ 2
i=1
m
^
∃x, y1 ...ym . VARm+1 (x, y1 ..., ym ) → x 6= yi , m ≥ 2
i=1
Lastly, the first sentence defines that one instance of a variation point is related
at least one variant or variation point through the predicate VARm+1 . The two last
sentences impose the same constraints than the previous variability types.
Now we define the dependencies REQ and EXC as follows. We write sentences for
only one relation REQ and only one EXC, while the remaining ones are defined by
replacing the types of services. Moreover, in both formulae, the ⊕ operator is semantic-
ally equivalent to the exclusive or (XOR) operation.
Requires: ∃x.REQ(x, y) → Svpk (y) ⊕ Svk (y)
Excludes: for any fixed k,
∃x.EXC(x, y) ∧ (Svpk (x) ⊕ Svk (x)) → ¬(Svpk (y) ∨ Svk (y))
∃x.EXC(x, y) ∧ (Svpk (y) ⊕ Svk (y)) → ¬(Svpk (x) ∨ Svk (x))
3.1 Reasoning Services
We have characterised SeVaTax diagrams in FOL in order to allow modellers to use
this formalisation for checking relevant properties over these diagrams. Some typical
services of interest are the followings:
Definition 2. Let Σ be a SeVaTax diagram and Σ F OL be the corresponding SeVaTax
Knowledge Base:
- Service consistency: A service S is consistent if the SeVaTax diagram admits an in-
stantiation in which S has instances. Formally, Σ F OL corresponding to Σ admits a
model in which S has a nonempty extension.
- SeVaTax consistency: A SeVaTax diagram is consistent if it admits an instantiation,
i.e. an actual choice of variants or variation points matching the constraints imposed
by the diagram such that some service is not empty. Formally, the set of FOL assertions
corresponding to the SeVaTax diagram admits a model in which some the service has
a nonempty extension. This means that at least one product might be derived from the
variability model. This reasoning service corresponds with the query Valid Model as
defined in section 2.
- Strong SeVaTax consistency: A SeVaTax diagram Σ is strongly consistent if for each
S (variant or variation point) the set of FOL assertions corresponding to the diagram
Σ F OL , admits some model such that S has a nonempty extension. This means that every
service in the variability model might be derived as part of at least one product.
- Dead Service: A service S (variant or variation point) is a dead service w.r.t. Σ F OL if
there is no model such that S has a nonempty extension. This means that some services
might never be derived as part of some product. This service corresponds with the query
Problems Detection as also defined in section 2.
Each service defined above can be reduced to each other [2]. Moreover, the service
consistency reasoning task amounts to checking if a given service can be instantiated
and corresponds to the notion of concept consistency DLs.
4 DL Encoding of SeVaTax Diagrams
We now define a DL formalisation of SeVaTax diagrams and prove the correctness
of the encoding. We only show the encoding for interactions between variation points
and variants so that the below assertions must be rewritten for the remaining possible
combinations. On the other hand, for sake of simplicity in this ongoing approach we
consider singleton DL classes to encode services. However, we are working in other
approaches using nominals or ABox facts to express atomic services and thus keeping
the upper bound of complexity under control.
Definition 3. Let Σ be a SeVaTax diagram. Σ ALCI is the DL Knowledge Base repres-
enting Σ and constructed as φ(Σ) = (A, R, T ) as follows:
– The set A of atomic concepts of φ(Σ) contains the elements below:
• an atomic concept φ(Svpi ) for each variation point Svpi .
• an atomic concept φ(Svj ) for each variant Svj .
– Let us suppose services S and Si in the SeVaTax diagram Σ related by a variability
type (S is related to Si ). Then the edge connecting the nodes S and Si is formalised
into an ALCI role rSi which represents the relation between φ(S) and φ(Si ). If
both S and Si in Σ are related by any of the Requires and Excludes dependencies
then the edge connecting the nodes S and Si is formalised into ALCI roles rRSi
and rESi , respectively. This means that each edge connecting services through any
variability type or dependency, as defined in section 2, is translated into a DL role.
– The set T of assertions of φ(Σ) contains the following elements:
φ(Svpi ) v ¬φ(Svpl ) φ(Svj ) v ¬φ(Svl ) 1 ≤ i ≤ n, 1 ≤ j ≤ m, i, j 6= l
• if Svpk MAND{Sv1 , ..., Svm } is in Σ, then (for each j and for any fixed k):
∃rSvj v φ(Svpk ) ∃rS−v v φ(Svj ) φ(Svpk ) v G ∃rSvj .φ(Svj )
j
1≤j≤m
φ(Svj ) v ∃rS−v .φ(Svpk ), for each φ(Svj ), 1 ≤ j ≤ m
j
• if Svpk OPT{Sv1 , ..., Svm } is in Σ, then (for each j and for any fixed k):
G
∃rSvj .φ(Svj ) v φ(Svpk )
1≤j≤m
and for each φ(Svj ) element playing the corresponding role rSvj :
φ(Svj ) v ∃rS−v .φ(Svpk ), for each φ(Svj ), 1 ≤ j ≤ m
j
• if Svpk ALT{Sv1 , ..., Svm } is in Σ, then (for each j and for any fixed k):
G !
φ(Svpk ) v ∃rSvj .φ(Svj ) u G ¬∃rSvl .φ(Svl )
1≤j≤m 1≤l≤m
j6=l
and for the only one φ(Svj ) element playing the corresponding role rSvj :
φ(Svj ) v ∃rS−v .φ(Svpk ), for each φ(Svj ), 1 ≤ j ≤ m
j
• if Svpk VAR{Sv1 , ..., Svm } is in Σ, then (for each j and for any fixed k):
G
φ(Svpk ) v ∃rSvj .φ(Svj )
1≤j≤m
For each φ(Svj ) element playing the corresponding role rSvj :
φ(Svj ) v ∃rS−v .φ(Svpk ), for each φ(Svj ), 1 ≤ j ≤ m
j
−
• if Svpk REQ Svl is in Σ, then: φ(Svpk ) v ∀rR Sl
.φ(Svl )
• if Svpk EXC Svl is in Σ, then (for any fixed k):
−
φ(Svpk ) v ¬(∃rESl .φ(Svl )) φ(Svl ) v ¬(∃rE S
.φ(Svpk ))
l
We now show that the encoding for the variability types in a Σ is correct. For this,
we establish a correspondence between models in Σ F OL KB and models of the corres-
ponding Σ ALCI KB.
Theorem 1. Let Σ be a SeVaTax diagram, Σ F OL the corresponding FOL formalisa-
tion and Σ ALCI the ALCI KB constructed as specified above. Then a service S is
consistent in Σ iff the corresponding concept φ(S) is satisfiable w.r.t. Σ ALCI .
Proof. [⇒] Let S be consistent service in Σ, then there exists a model of Σ F OL in
which S has a nonempty extension. Let O = (∆O , .O ) be a model of Σ F OL such that
S O 6= ∅. We build a model I = (∆I , .I ) of Σ ALCI such that φI (S) 6= ∅, as follows:
– ∆I = ∆ O
– φI (Svpi ) = Svp
O
i
, for each φ(Svpi ) corresponding to services Svpi ∈ Σ
I O
– φ (Svj ) = Svj , for each φ(Svj ) corresponding to services Svj ∈ Σ
– RI are all the ALCI-roles corresponding to variability types and dependencies.
Each role rSIj modelling the relation between the first and the jth component of any
n + 1-ary variability type (for each arbitrary n), is defined as follows.
• rSIj = {(s0 , sj )} such that (s0 , s1 , ..., sn ) ∈ MANDn+1(I) , 1 ≤ j ≤ n
• rSI 0 = {(s00 , s0j )} such that (s00 , s01 , ..., s0n ) ∈ OPTn+1(I) , 1 ≤ j ≤ n
j
• rSI 00 = {(s000 , s00j )} such that (s000 , s001 , ..., s00n ) ∈ ALTn+1(I) , 1 ≤ j ≤ n
j
n+1(I)
• rSI 000 = {(s000 000 000 000 000
0 , sj )} such that (s0 , s1 , ..., sn ) ∈ VAR , 1≤j≤n
j
RI also includes rRSj and rESj for the variability dependencies REQI and EXCI .
It is immediate to check that I satisfies all the assertions in Σ ALCI . We detail the
proof for the Mandatory variability type associating a variant point to only variant
services, since the remaining possible types and dependencies are similarly proved.
Let S be a variation point. As it is consistent in Σ, S O 6= ∅. Then, there exists a
variability type or dependency in which S participates. Let us suppose that this variab-
ility type is mandatory. So, there must exist variants s1 , ..., sn ∈ ∆O ,and Svi (si ) and
MAND(s0 , s1 , ..., sn ) hold. Moreover:
– by definition of R, there exist rSIj roles relating s0 with each sj . As s0 ∈ φI (Svp0 )
and sj ∈ φI (Svj ) for each j, thus both ∃rSj v φ(Svp0 ) and ∃rS−j v φ(Svj ) hold.
– φI (Svp0 ) participates in the mandatory association through roles rSIj and as φI (Svj ) 6=
∅ for all j, each second element of each rSIj is a element φI (Svj ), then φ(Svp0 ) v
F 1≤j≤n ∃rSvj φ(Svj ) holds.
– Conversely, each existing φI (Svj ) participates in the corresponding rSIj , whose
first element is also φI (Svp0 ), for each j. Then the assertion φ(Svj ) v ∃rS−j .φ(Svp0 )
holds.
Hence, I satisfies the corresponding ALCI assertions for the Mandatory variab-
ility type. The proof is similar if we consider variation points instead of variant in the
mandatory variability. Moreover, the same proof applies to the remaining variability
types and dependencies.
[⇐] By the tree-model property, if φ(S) is satisfiable w.r.t. the Σ ALCI KB then
there exists a tree-like model I = (∆I , .I ) of Σ ALCI such that φI (S) 6= ∅. From such
a tree-like model we can build an instantiation O = (∆O , .O ) of Σ such S O 6= ∅ as
follows.
– ∆O = Svp ∈VP φI (Svp ) Sv ∈V φI (Sv ), where VP and V denote the set of vari-
S S
ation points and variants of Σ, respectively.
O
– Svp i
= φI (Svpi ), for all service Svpi in Σ.
– Svj = φI (Svj ), for all service Svj in Σ.
O
– REQO = rRSj , rRSj ∈ RI for each Requires dependency in Σ
– EXCO = rESj , rESj ∈ RI for each Excludes dependency in Σ
Vn
– MANDn+1(O) = {(s0 , s1 , ..., sn ) | i=1 (s0 , sj ) ∈ rSIj }
n
– OPTn+1(O) = {(s0 , s1 , ..., sn ) | i=1 (s0 , sj ) ∈ rSIj }
V
n
– ALTn+1(O) = {(s0 , s1 , ..., sn ) | i=1 (s0 , sj ) ∈ rSIj }
V
n
– VARn+1(O) = {(s0 , s1 , ..., sn ) | i=1 (s0 , sj ) ∈ rSIj }
V
Observe that, since O is a tree-like model, it is guaranteed that there is only one
O
object s0 ∈ Svp that represents a variation point. Hence, by definition of mandatory
dependency there must also exist the elements sj ∈ SvOj representing tuples for this
type so as the FOL assertions for MAND(s0 , s1 , ...sn ) hold. Similarly for the other
variability types and dependencies. Finally, O correctly instantiates Σ. t
u
Theorem 2. Reasoning over SeVaTax schemes is EXPTIME w.r.t. SeVaTax service con-
sistency.
Proof. By theorem 1 and ALCI complexity [1]. t
u
Example 2. Before ending this section, we revisit the example 3 in order to show the DL
encoding for the SeVaTax diagram showing the use of the mandatory variability type
for the Connectivity VP. The ALCI encoding for mandatory type is the following:
∃rW IF I v Connectivity ∃rU SB v Connectivity ∃rBluetooth v Connectivity
− − −
∃rW IF I v W IF I ∃rU SB v U SB ∃rBluetooth v Bluetooth
Connectivity v ∃rW IF I .W IF I u ∃rU SB .U SB u ∃rBluetooth .Bluetooth
− −
Connectivity v ∃rW IF I .W IF I Connectivity v ∃rU SB .U SB
−
Connectivity v ∃rBluetooth .Bluetooth
5 Related Works
Table 1 compares main works in the literature proposing variability analysis of FMs
due to, at the best of our knowledge, there does not exist any work embedding other
modelling approaches in DL. Thus, the second column of the table shows the formal
model (F.M.) used by each proposal, the third one indicates the reasoners, and the last
columns describe the questions which reasoners should be capable of answer [16, 17, 3].
On the other hand, it does exist proposals integrating OVM and SAT solvers [20, 28],
however, they present the same drawbacks explained in section 1. Then, we conclude
this section only detailing the related works whose proposals embed FMs in DL.
Aproach F.M. Reasoner
Verify
VM VI AP NP PD
Wang et al. [34] OWL FACT++ x x - - x
Noorian et al. [21] DL Pellet x x - - x
Fan et al. [8] DL Racer x x - - -
Das et al. [7] OWL-DL RACER x x - - x
Ripon et al.[26] OWL-DL RACER x x - - x
Ryssel et al. [29] OWL-CSP FACT++ x x - - -
Rincon et al. [25] OWL - SQWRL JESS x x - - x
Zaid et al. [35] OWL-DL SWRL Pellet x x - - x
Table 1. Summary of Semantic Analysis Process of Variability Models
In Table 1, we can see the work of Wang et. al [34] in which authors propose a
method for formalising FMs into OWL [9], by using a prototype tool (that in future
works will be available as a Protégé [15] plugin. Then, a FACT++ reasoner [33] is
used for problem detection by providing a debugger module, which identifies the most
general conflicts and gives an explanation. Noorian et.al [21] present a translation of
FMs into DL, and use Pellet [30] and a Reiter’s algorithm [24] for solving two types
of inconsistencies (applied to structural and integrity constraints). In Fan & Zhang [8]
authors present a set of translation rules for building DL knowledge bases ALCQI from
FMs. Then, the consistency of these models is checked by using the RACER reasoner
[10]. In Das et al. [7] and Ripon et al. [26] the consistency and detection of inconsistent
classes are evaluated according to the responses of the RACER reasoner. In Rincon et
al. [25] authors detect dead and false optional features and explain the causes in natural
language. Finally, Zaid et al. [35] detect specific classes generating inconsistencies by
the set of rules defined in SWRL [12] over the OWL model.
As we can see, none of the analysed works makes an analysis of All Products (AP)
and Instantiation Number (IN) queries, which are two of the most common queries
needed in any variability analysis process. At the same time, more specific queries [16,
17, 3] are not analysed either.
6 Conclusions and Future Work
The well-known benefits of using DL to conceptual representation admitting decid-
able reasoning fit with the requirements for implementing an automated variability ana-
lysis process for the SeVaTax framework. The contributions of this work are twofold.
Firstly, the formalisation of OVM-based SeVaTax model expressed in first order logic
and secondly, a novel ALCI encoding allowing reasoning over SeVaTax. Moreover, we
establish the EXPTIME-membership of reasoning on its diagrams w.r.t. service consist-
ency. Until now such a formalisation of OVM-based diagrams had not been done.
As future work, we plan to continue extending reasoning capabilities of our frame-
work. Additionally, we are currently developing a prototype providing a back-end for
the automated support of consistency checking of SeVaTax diagrams along with its
encoding into DL knowledge bases.
References
1. Artale, A., Calvanese, D., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Reasoning over
Extended ER Models. In: Conceptual Modeling - ER 2007, 26th International Conference
on Conceptual Modeling, Auckland, New Zealand (2007)
2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The
Description Logic Handbook: Theory, Implementation, and Applications. Cambridge Uni-
versity Press, New York, NY, USA (2003)
3. Benavides, D., Segura, S., Ruiz-Cortés, A.: Automated Analysis of Feature Models 20 Years
Later: A Literature Review. Inf. Syst. 35(6), 615–636 (Sep 2010)
4. Brisaboa, N.R., Cortinas, A., Luaces, M.R., Pol’la, M.: A Reusable Software Architecture for
Geographic Information Systems Based on Software Product Line Engineering. In: Model
and Data Engineering - 5th International Conference, MEDI 2015, Rhodes, Greece, Septem-
ber 26-28, 2015, Proceedings. pp. 320–331 (2015)
5. Buccella, A., Cechich, A., Pol’la, M., Arias, M., Doldan, S., Morsan, E.: Marine ecology
service reuse through taxonomy-oriented spl development. Computers & Geosciences –(0),
In press (2014)
6. Buccella, A., Cechich, A., Arias, M., Pol’la, M., del Socorro Doldan, M., Morsan, E.: To-
wards systematic software reuse of gis: Insights from a case study. Computers & Geosciences
54(0), 9 – 20 (2013)
7. Das, N.C., Ripon, S., Hossain, O., Uddin, M.S.: Requirement Analysis of Product Line Based
Semantic Web Services. Lecture Notes on Software Engineering (2014)
8. Fan, S., Zhang, N.: Feature Model Based on Description Logics, pp. 1144–1151. Springer
Berlin Heidelberg, Berlin, Heidelberg (2006)
9. Grau, B.C., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P., Sattler, U.: OWL 2: The
Next Step for OWL. Web Semant. 6(4), 309–322 (Nov 2008)
10. Haarslev, V., Möller, R.: RACER System Description. In: Goré, R., Leitsch, A., Nipkow, T.
(eds.) International Joint Conference on Automated Reasoning, IJCAR’2001, June 18-23,
Siena, Italy. pp. 701–705. Springer-Verlag (2001)
11. Haugen, O., Moller-Pedersen, B., Oldevik, J., Olsen, G.K., Svendsen, A.: Adding Standard-
ized Variability to Domain Specific Languages. In: 2008 12th International Software Product
Line Conference. pp. 139–148 (2008)
12. Horrocks, I., Patel-Schneider, P.F., Bechhofer, S., Tsarkov, D.: OWL Rules: A Proposal and
Prototype Implementation. Web Semant. 3(1), 23–40 (Jul 2005)
13. Janota, M.: Do SAT Solvers Make Good Configurators? In: Software Product Lines, 12th In-
ternational Conference, SPLC 2008, Limerick, Ireland, September 8-12, 2008, Proceedings.
Second Volume (Workshops) (2008)
14. Kang, K., Cohen, S., Hess, J., Nowak, W., Peterson, S.: Feature-Oriented Domain Analysis
(FODA) Feasibility Study. Technical Report CMU/SEI-90-TR-21, Software Engineering In-
stitute, Carnegie Mellon University Pittsburgh, PA. (1990)
15. Knublauch, H., Fergerson, R., Noy, N., Musen, M.: The Protégé OWL plugin: An open
development environment for semantic web applications (2004)
16. Kowal, M., Ananieva, S., Thüm, T.: Explaining Anomalies in Feature Models. In: Proceed-
ings of the 2016 ACM SIGPLAN International Conference on Generative Programming:
Concepts and Experiences. GPCE 2016, ACM, New York, NY, USA (2016)
17. von der Massen, T., H. Lichter, H.: Deficiencies in Feature Models. In: Mannisto, T., Bosch,
J. (eds.) Workshop on Software Variability Management for Product Derivation - Towards
Tool Support (2004)
18. Mendonca, M., Cowan, D.: Decision-making coordination and efficient reasoning techniques
for feature-based configuration. Science of Computer Programming (2010), coordination
Models, Languages and Applications (SAC’08)
19. Mendonca, M., Wasowski, A., Czarnecki, K.: SAT-based Analysis of Feature Models is Easy.
In: Proceedings of the 13th International Software Product Line Conference. pp. 231–240.
SPLC ’09, Carnegie Mellon University, Pittsburgh, PA, USA (2009)
20. Metzger, A., Pohl, K., Heymans, P., Schobbens, P.Y., Saval, G.: Disambiguating the Docu-
mentation of Variability in Software Product Lines: A Separation of Concerns, Formalization
and Automated Analysis. In: 15th IEEE International Requirements Engineering Conference
(RE 2007). pp. 243–253 (Oct 2007)
21. Noorian, M., Ensan, A., Bagheri, E., Boley, H., Biletskiy, Y.: Feature Model Debugging
based on Description Logic Reasoning. In: Proceedings of the 17th International Conference
on Distributed Multimedia Systems, DMS 2011, October 18-20, 2011, Convitto della Calza,
Florence, Italy. pp. 158–164 (2011)
22. Pohl, K., Böckle, G., Linden, F.J.v.d.: Software Product Line Engineering: Foundations, Prin-
ciples and Techniques. Springer-Verlag New York, Inc., Secaucus, NJ, USA (2005)
23. Pol’la, M., Buccella, A., Arias, M., Cechich, A.: SeVaTax: service taxonomy selection val-
idation process for SPL development. In: 2015 34th International Conference of the Chilean
Computer Science Society (SCCC). pp. 1–6 (Nov 2015)
24. Reiter, R.: A Theory of Diagnosis from First Principles. Artif. Intell. 32(1), 57–95 (Apr 1987)
25. Rincón, L.F., Giraldo, G.L., Mazo, R., Salinesi, C.: An Ontological Rule-Based Approach
for Analyzing Dead and False Optional Features in Feature Models. Electron. Notes Theor.
Comput. Sci. (2014)
26. Ripon, S., Piash, M.M., Hossain, S.M.A., Uddin, M.S.: Semantic Web Based Analysis of
Product Line Variant Model. JCEE 2014 6(1), 1–6 (2014)
27. Roos-Frantz, F., Galindo, J.A., Benavides, D., Cortés, A.R., Garcıa-Galán, J.: Automated
analysis of diverse variability models with tool support. Jornadas de Ingenierıa del Software
y de Bases de Datos (JISBD 2014), Cádiz. Spain p. 160 (2014)
28. Roos-Frantz, F., Galindo, J.A., Benavides, D., Ruiz-Cortés, A.: FaMa-OVM: A Tool for the
Automated Analysis of OVMs. In: Proceedings of the 16th International Software Product
Line Conference - Volume 2. SPLC ’12, ACM, New York, NY, USA (2012)
29. Ryssel, U., Ploennigs, J., Kabitzsch, K.: Reasoning of Feature Models from Derived Fea-
tures. In: Proceedings of the 11th International Conference on Generative Programming and
Component Engineering. GPCE ’12, ACM, New York, NY, USA (2012)
30. Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A practical owl-dl reasoner.
Web Semant. 5(2), 51–53 (Jun 2007)
31. Sree-Kumar, A., Planas, E., Clarisó, R.: Analysis of Feature Models Using Alloy: A Survey.
In: Proceedings 7th International Workshop on Formal Methods and Analysis in Software
Product Line Engineering, FMSPLE@ETAPS 2016, Eindhoven, The Netherlands, April 3,
2016. pp. 46–60 (2016)
32. Sun, J., Zhang, H., Li, Y.F., Wang, H.: Formal Semantics and Verification for Feature Model-
ing. In: ICECCS ’05: Proceedings of the 10th IEEE International Conference on Engineering
of Complex Computer Systems (ICECCS’05). IEEE Computer Society (2005)
33. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: In
Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006. pp. 292–297. Springer
(2006)
34. Wang, H.H., Li, Y.F., Sun, J., Zhang, H., Pan, J.: Verifying Feature Models Using OWL. Web
Semant. 5(2), 117–129 (Jun 2007)
35. Zaid, L.A., Kleinermann, F., De Troyer, O.: Applying Semantic Web Technology to Feature
Modeling. In: Proceedings of the 2009 ACM Symposium on Applied Computing. SAC ’09,
ACM, New York, NY, USA (2009)