=Paper=
{{Paper
|id=Vol-2211/paper-26
|storemode=property
|title=Verifying Contract-Based Specifications of Product Lines using Description Logic
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-26.pdf
|volume=Vol-2211
|authors=Damir Nešić,Mattias Nyberg
|dblpUrl=https://dblp.org/rec/conf/dlog/NesicN18
}}
==Verifying Contract-Based Specifications of Product Lines using Description Logic==
https://ceur-ws.org/Vol-2211/paper-26.pdf
Verifying Contract-Based Specifications of
Product Lines using Description Logic
Damir Nešić1 and Mattias Nyberg1,2
1
Royal Institute of Technology, Stockholm, Sweden
2
Scania CV AB, Södertalje, Sweden
{damirn,matny}@kth.se
Abstract. The complexity of critical systems is constantly increasing
and if developed as Product Lines (PLs), the number of possible sys-
tem configuration can be huge. Consequently, assuring system properties
such as safety or security is increasingly difficult. Assurance cases are
used often to argue that a system is safe or secure and Contract-Based
Specification models are a promising foundation for assurance case ar-
gumentation. This paper defines a method for Description Logic (DL)
based verification of the well-formedness constraints of an arbitrary CBS
model of a PL. The paper presents the DL encoding of arbitrary CBS
model, the DL encoding of the well-formedness constraints, and shows
how the verification of these constraints can be reduced to satisfiability
verification of the corresponding knowledge base. In order to validate the
presented approach, a small, but real, industrial PL was expressed as
a CBS model, implemented as an OWL ontology, and an off-the-shelf
reasoner was used to verify if the CBS model is well-formed.
1 Introduction
The complexity and heterogeneity of critical systems from domains such as
automotive or aerospace is constantly increasing [15]. Furthermore, in order to
increase the portfolio of products, critical systems are designed by following the
Product Line Engineering (PLE) paradigm [2], which facilitates the development
of a Product Line (PL) of similar systems such that a high number of distinct
system configurations is possible. As a consequence, assuring that the complete
PL satisfies properties like safety or security is increasingly difficult and in the
case of a very high number of configurations even not feasible [16, 24, 38].
Development of critical systems is regulated by various standards [19, 20], and
often the proof of compliance is embodied in a form of an assurance case. An
assurance case is a ”a reasoned and compelling argument, supported by a body
of evidence, that a system [...] will operate as intended for a defined application
in a defined environment” [1]. Developing the assurance case argumentation-
structure and identifying the appropriate evidences are both difficult tasks. The
required ”body of evidence” are concrete engineering artifacts, such as results
of safety analyses, specifications, test cases etc. These are usually maintained
and evolved by different tools, which in an enterprise setting often leads to
inconsistencies among these artifacts. As argued in [5, 27], Semantic Web [32],
2 D. Nešić and M. Nyberg
and Linked Data [9] are promising approaches for cleaning and integrating such
heterogeneous data with the purpose of creating a reliable source of knowledge,
e.g. a source of assurance case evidences.
Difficulties regarding the assurance case argumentation-structure stem from
the fact that arguing that a system is safe or secure can only be done based on the
methods used to engineer the system. Typically, a variety of methods with different
semantics and levels of formality are used to specify, design, implement, and
verify a PL of systems. Consequently, constructing a ”reasoned and compelling”
argumentation-structure is challenging and most often manual. One of the few
approaches that can serve as a unifying framework for specification, design,
and input for verification of complex, heterogeneous PLs is the Contract-Based
Specification (CBS) framework [8, 30, 37] and its PLE extension [26]. As briefly
discussed in [8], and as shown in [34] with basic CBS concepts, a CBS model of
a system can serve as the foundation for assurance case argumentation.
In order to use a CBS model for this purpose, the model must conform to
various constraints which ensure sound and complete argumentation. Although
these constraints can be verified using various technologies, the present paper
introduces an approach based on Description Logic (DL) [4]. Because DL is the
foundation of the Web Ontology Language (OWL) [23], which is a part of the
Semantic Web stack, the aim of the paper is to enable the verification of CBS
models, and indirectly the assurance case arguments, with technologies that are
tightly coupled with technologies that can be used for assurance-case evidence
access. Consequently, this should reduce the effort of automating the prevailingly
manual process of assurance case construction. The results show that using DL
for the verification of CBS models is possible, and also that formalizing the
semantics of PLE and CBS concepts in DL is intuitive. However, the results also
show that the open-world assumption and the lack of support for meta-modeling,
incur overhead in the encoding of CBS models as a DL Knowledge Base (KB).
Literature on using DL and DL-based reasoners for analyzing contract-based
models is rare. Somewhat related work is [22, 39] where the issue of automatically
brokering contracts between web services is treated. However the notion of a
contract and its use is different and less formal compared to CBS frameworks.
Most notable non DL-based work regarding analysis of contract-based models is
the MICA tool [11]. While the present paper focuses on verifying CBS models of
PLs independent of the formalism for expressing contracts, the MICA tool focuses
on fine-grained analyses of CBS models expressed using modal interface theory.
Interestingly, OWL has been extensively used in PLE as a tool for the analysis of
the so-called variability models, which represent the commonality and variability
of a PL. Work in [31] encodes a set of Simulink [13] objects that represent PL
variations, as a DL KB and uses an off-the-shelf reasoners to analyze the possible
product configurations for various defects [7]. Approaches in [14, 28, 36] provide
the encoding of a particular type of a variability model, the so-called feature
model (FM) [6], as a DL KB and also use off-the-shelf reasoners to detect similar
product configuration defects. The approach in [10] performs a similar task but
instead of an FM, the considered variability model is an OVM model [29]. The
present paper also encodes an arbitrary FM as a DL KB but because the purpose
Verifying Contract-Based Specifications of Product Lines using DL 3
of the FM encoding is to support the analysis of CBS models, the DL semantics
of FM constructs is different and the encoding is more compact.
Paper Structure. Section 2 summarizes the concepts underlying PLE, CBS and
the constraints to be verified against an arbitrary CBS model. Section 3 defines
the semantics of presence conditions in terms of CBS concepts. Section 4 presents
the encoding of the PLE and CBS concepts as a DL KB and it is followed by
Section 5 which exemplifies how an arbitrary CBS model can be verified against
the defined constraints. Finally, Section 6 concludes the paper.
2 Background
The idea behind PLE is to declare features [2] which represent characteristics of
each product in a PL, and express them, and their mutual dependencies, in a
variability model which is most often a Feature Model (FM). This representation
of a PL is a part of the so-called problem space [3]. Given an FM, development
artifacts are labeled with feature-based formulas referred to as presence conditions.
The representation of a PL in terms of artifacts labeled with presence conditions is
referred to as the solution space [3]. By selecting features from an FM, a particular
product configuration is selected, and the set of artifacts that implement the
selected product configuration are those whose presence conditions evaluate to
true for the given feature selection. The remainder of this section presents FMs
as the solution space and CBS models, as the problem space representation of a
PL. From here on, a feature is considered to be a Boolean variable.
2.1 Feature models and presence conditions
Definition 1 (Feature Model). A feature model V is a pair V = (F, C) where
F = {f1 , . . . , fn } is a set of features and C is a set of Boolean constraints over
the features in F.
FMs define graphical syntax for a set of Boolean constraints in order to
structure the features into a tree, where each parent-fi to child -fm relation
corresponds to the expression fm → fi . Figure 1a shows the FM graphical
syntax used in the present paper, together with corresponding propositional
expressions [12]. Figure 1b shows the FM running example, created using the
FeatureIDE tool [21]. The syntax in Figure 1a is read as: i) fm is a mandatory
feature, ii) fm and fn are a group of alternative features where Y stands for
exclusive or, iii) fm and fn are a group of or features, and iv) fm is an optional
feature. Note that Figure 1b contains additional Boolean constraints, where the
constraint such as V8 → Advanced is read as requires.
Definition 2 (Product Configuration). Given a feature model V = (F, C), a
product configuration, denoted as PC , is a set of feature value-assignments such
that each fi ∈ F is assigned with a value true or false. A product configuration
for which each Boolean constraint in C evaluates to true is valid.
A product configuration represents, in terms of features, all individual systems
that are identically configured. As discussed previously, the feature representation
is mapped to the representation in terms of concrete artifacts by labeling the
artifacts with presence conditions.
4 D. Nešić and M. Nyberg
fi fi fi fi
i) ii) iii) iv)
fm fm fn fm fn fm
fi → fm fi → (fm Y fn )fi → (fm ∨ fn )
(a) Used FM graphical syntax. (b) FM running example.
Fig. 1: Used FM constructs and the FM running-example.
Definition 3 (Presence Condition). A presence condition ϕ is a Boolean
expression over features in F, defined as ϕ ::= fi |¬(ϕ)|(ϕ ∧ ϕ)|(ϕ ∨ ϕ).
2.2 Contract-Based Specification and Design
The basic concepts of CBS are shown in Figure 2a. Given these, the central
concept of a Contract is defined as following.
Definition 4 (Contract). A Contract K is an ordered pair of specifications,
denoted (A, G), where A is called an Assumption, G is called a Guarantee, and A
and G are in the assumption of relation, denoted assumptionOf(A, G).
A component C satisfies a contract K = (A, G) if for each component C 0 such
that implements(C 0 , A), the component C 00 is such that implements(C 00 , G) where
composedOf(C 00 , C 0 ) and composedOf(C 00 , C). Components composed of other
components are referred to as Composite while components not composed of
other components are referred to as Atomic. The expectation that a component C
shall satisfy the contract K is indicated by allocating a contract to a component,
denoted as allocatedTo(K, C). Finally, in order to allow PLs, function Φ labels
each Specification and each Component with a presence condition ϕ. Figure 2b
shows the running example which is the Fuel Level Display system (FLD), a real
system present in product of Scania CV AB.
Basic CBS concepts
Component C - Physical or logical component
Specification S - Requirement on C behaviour
implements(C, S) - C behaviour conforms to S
fulfills(Si , Sj ) - ∀C.implements(C, Si ) →
implements(C, Sj )
composedOf(C, C1 ) - C1 comprises C
a
Detailed descriptions can be found in [26].
(a) Basic CBS concepts (b) FLD system running example.
Fig. 2: Basic CBS concept (left) and the running CBS model example (right)
The composite component FLD is composed of atomic components FuelSensor,
COO, short for COOrdinator, BMS, short for Body Management System, and ICL,
Verifying Contract-Based Specifications of Product Lines using DL 5
short for Instrumentation CLuster. Relations fulfills are shown as arrows labeled
f, relations assumptionOf are shown as arrows labeled a, and white rectangles
represent contracts. Overlaying a contract over a component represents the
allocatedTo relation. The intended functionality of the FLD system is to display
the current fuel level on the ICL display and guarantee that the displayed value
corresponds to the actual fuel level. Guarantee G0 captures this specification
under the assumption A0 that the ignition key is turned on.
The guarantees of contracts allocated to FuelSensor, COO, BMS and ICL specify
that the fuel level measurement in volts, its conversion to liters, and its display
on a [0 − max] scale, correspond to the actual fuel level, while assuming that
the power-supply is nominal, that the information on the communication buss
is updated regularly etc. Consequently, if G3 is implemented, i.e. the displayed
value corresponds to the actual one, then G0 is implemented, i.e. G3 fulfills G0 .
The dashed border of BMS and COO indicates that these components are not
present in each product configuration, i.e. COO is responsible for volts to liters
conversions in product configurations with diesel fuel, while BMS, performs the
same conversion in product configurations with gas fuel. In other words, the CBS
model in Figure 2b defines the solution space of a PL of FLD systems.
If a CBS model of a PL conforms to certain constraints, then it is referred to
as a specification structure.
Definition 5 (Specification Structure). Given a set of contracts Ki = (Ai , Gi ),
where each Ai and Gi is unique, such that each Ki is allocated to a single atomic
component Ci , a contract K 0 = (A0 , G0 ) allocated to the composite component
C 0 , which is composed of atomic components Ci , an edge-labeled directed graph
D = (N , E) is a specification structure if:
i) each node n ∈ N is either an assumption Ai or A0 or a guarantee Gi or G0 ,
ii) each edge e = (ni , nj ) ∈ E corresponds to either a single assumptionOf(Si , Sj )
or a single fulfills(Si , Sj ) relation,
iii) for each edge e = (ni , nj ) ∈ E it holds that ni 6= nj ,
iv) for each assumptionOf(Si , Sj ) relation, Si is an assumption, Sj is a guarantee
and the ordered pair (Si , Sj ) is a contract,
v) for each edge fulfills(Si , Sj ), if
a) Si is a guarantee then Si is a guarantee of a contract Ki and Sj is either
an assumption Aj or the guarantee G0 ,
b) Si is an assumption then Si is the assumption A0 and Sj is any Ai .
Definition 5 allows circular specification structures, or presence conditions
of an assumption A and a guarantee G of a contract (A, G) such that in some
product configurations A and G do not simultaneously apply. To avoid such cases,
a proper specification structure is defined. The entailment between presence
conditions ϕi and ϕj is denoted as ϕi |=C ϕj as a short hand for (C, ϕi ) |= ϕj , i.e.
entailment must hold under the constraints from C. For example, in Figure 2b, it
holds that ϕ2 2 ϕ1 , but when constraints Truck → Fuel and Fuel → Gas Y Diesel
from Figure 1b are considered, then the entailment holds, i.e. ϕ2 |=C ϕ1 .
Definition 6 (Proper Specification Structure). Given a feature model V =
(F, C), a specification structure is proper if:
6 D. Nešić and M. Nyberg
i) for each assumption Ai of a contract Ki , there exists a specification Sk such
that fulfills(Sk , Ai ), where Sk is either A0 or Gi ,
ii) there exists a guarantee Gi such that fulfills(Gi , G0 ),
iii) the graph of D is acyclic,
iv) for each contract (Ai , Gi ), it holds that Φ(Ai ) |=C Φ(Gi ) and Φ(Gi ) |=C Φ(Ai ),
v) for each contract (Ai , Gi ) allocated to a component Ci it holds that Φ(Ai ) |=C
Φ(Ci ) and Φ(Gi ) |=C Φ(Ci ),
vi) for the composite component C 0 composed of atomic components Ci , for each
Ci it holds that Φ(Ci ) |=C Φ(C 0 ),
vii) for each contract Ki = (Ai , Gi ) allocated to an atomic component Ci and
for each specification Sk such that fulfills(Sk , Ai ) it holds that Φ(Ai ) |=C
W
fulfills(Sk ,Ai ) Φ(Sk ),
viii) for the contract K 0 = (A0 , G0 ) allocated to the composite component C 0 and
for each guarantee Gi of a contract Ci such that fulfills(Gi , G0 ) it holds that
0
W
Φ(G ) |=C fulfills(Gi ,G0 ) Φ(Gi ).
The following theorem presents the key compositional idea of the CBS [26].
Note that in the following theorem, symbol |= means entailment between Si , Sj
irregardless of the formalisms used to express Si and Sj .
Theorem 1. Given a feature model V, and a specification structure D, if
i) D is proper,
ii) for each relation fulfills(Si , Sj ), it holds that Si |= Sj ,
iii) each atomic component Ci satisfies the contract allocated to it,
then, for each valid product configuration PCi , the composite component C 0
satisifes the contract K 0 .
Less formally, if a CBS model of a PL is a proper specification structure, and
if each pair of specifications in fulfills relation entail each other, then by verifying
that each component of each PL product configuration satisfies the contract
allocated to it, it can be inferred that each product configuration satisfies the
contract allocated to it. The remainder of the paper shows how to verify that an
arbitrary CBS model, is a proper specification structure.
3 Semantics of presence conditions
This and the following sections present the contribution of the paper. In order to
be able to verify that an arbitrary CBS model is a proper specifications structure,
it is necessary to define a common semantic interpretation of the constructs
representing the problem space and the solution space.
Because an FM and a CBS model jointly represent the PL design, a potentially
infinite number of product individuals p can be created by instantiating the PL
design. From this it follows that each product configuration corresponds to a set
of products individuals. Furthermore, each p can be represented as a Component,
either atomic or composite. For example, each individual Scania product, which
is a truck or a bus, is a Composite component composedOf an individual of the
FLD system, which is also a Composite component.
Verifying Contract-Based Specifications of Product Lines using DL 7
Let Config be a function which given a product individual p returns its product
configuration PC . Moreover, let Eval be a function that takes a presence condition
ϕ and a product configuration PC and returns the value of ϕ for the given PC .
Definition 7 (Presence condition semantics). The semantics of a presence
condition ϕ, denoted as JϕK, is JϕK = {p| Eval(ϕ, Config(p)) = true}.
A presence condition ϕ corresponds to a set of individual products to which
the artifact labeled with ϕ applies. This interpretation of presence conditions
corresponds to the concept of product groups [25].
4 Encoding an FM and a CBS model as Tbox axioms
This section presents the encoding of an arbitrary FM and an arbitrary CBS
model as a set of Tbox axioms. In order to provide a formal encoding, a CBS
model is represented as a tuple M = (O, R, J·KT ), where O is a set of objects,
R is a set of pairs representing relations, and J·KT is a function which returns
the type of an object or a relation. For instance, a fragment of the example
from Figure 2b would be {G1 , A2 } ⊆ O, (G1 , A2 ) ∈ R, and GT1 = Specification,
AT1 = Specification, (G1 , A1 )T = fulfills.
Regarding DL notation, let NC , NR and NI be mutually disjoint sets of
concept names, role names, and individual names, respectively. In the remainder
of the paper we use the DL notation and the semantics defined in [4].
4.1 General CBS entities and relations as Tbox axioms
Before defining the encoding of a FM or a model M, the Tbox is complemented
with concepts and roles that correspond to general CBS entities and relations
and these are shown in Table 1. Roles RhasS , RhasA , RhasG , correspond to the
containment relation between a specification structure and specifications, de-
noted hasSpecification(D, Si ), and the containment relation between contracts
and corresponding assumptions and guarantees, denoted hasAssumption(K, A)
and hasGuarantee(K, G). The role Rcomp , short for comprises, represents the re-
lation inverse to composedOf, and roles RaPartOf , RgPartOf , RfullBy are inverse to
roles RhasA , RhasG , Rfulls , respectively. As will be shown later, expressing several
conditions from Definition 5 and Definition 6 will require these roles.
According to the discussion in Section 3, the Tbox is complemented with
the concept DP ∈ NC which represents all individual products, and the axiom
DP v DC in order to capture the fact that each individual product is a component.
Moreover, because specifications are partitioned into assumptions and guarantees,
the axiom DS ≡ DSA t DSG is added to the Tbox. Similarly, because components
are partitioned into Atomic and Composite components, the axiom DC ≡ DCA t
DCC is added to the Tbox.
Finally, Definition 4 and condition (iii) from Definition 5 can be encoded
as Tbox axioms independently of the provided FM or a model M. The axiom
DK v = 1 RhasA .DSA u = 1 RhasG .DSG corresponds to Definition 4, and ax-
ioms ∃ RassOf .Self v ⊥ and ∃ Rfulls .Self v ⊥ correspond to condition (iii) of
Definition 5. The semantics of the construct ∃R.Self is defined in [17].
8 D. Nešić and M. Nyberg
Table 1: Concepts and roles corresponding to CBS concepts and relations.
(a) Concepts Dx ∈ NC (b) Roles Rx ∈ NR
CBS entity concept Inclusion Role Domain Range Inverse
Spec. Struct. DSS Rfulls d:DS r:DS
Specification DS RassOf d:DSA r:DSG
Assumption DSA DSA v DS RalcTo d:DK r:DC
Guarantee DSG DSG v DS Rcomp d:DCA r:DCC
Component DC RhasA d:DK r:DSA
Composite Comp. DCC DCC v DC RhasG d:DK r:DSG
Atomic Comp. DCA DCA v DC RhasS d:DSS r:DS
Contract DK RgPartOf d:DSG r:DK RhasG
RaPartOf d:DSA r:DK RhasA
Disjoint: DSA u DSG v ⊥, DCC u DCA v ⊥
RfullBy d:DS r:DS Rfulls
Disjoint: DSS , DS , DC , DK are pairwise disjoint
a
Actual axioms available in [26].
4.2 Arbitrary FM as Tbox axioms
In order to verify conditions (iv)-(viii) from Definition 6, it is necessary to
consider the FM. Several publications [14, 28, 36] have encoded an FM as a set of
Tbox axioms that capture the FM graph in order to verify properties [7] of the
possible product configurations. The present paper encodes the FM differently
and the semantics of each feature f is a set of product individuals whose product
configuration PC is such that (f = true) ∈ PC . Consequently, the semantics of
concepts based on features, e.g. presence conditions or product configurations, is
also set of product individuals, just as the intuition suggests. The Tbox encoding
of an arbitrary FM V = (F, C) is shown in Table 2.
Table 2: FM as Tbox axioms.
FM construct Tbox encoding
Feature fi Dfi ∈ NC , Dfi v DP
Parent fi - child fm Dfm v Dfi
Parent fi - mandatory child feature fm Dfi v Dfm
Parent fi - optional child feature fm -
Parent fi - alternative feature group f1 , . . . , fn Dfi ≡ tn
j=1 Dfj ,Dfj u Dfk6=j v ⊥
Parent fi - or feature group f1 , . . . , fn Dfi ≡ tn
j=1 Dfj
Feature fi requires feature fj Dfi v Dfj
Encoding arbitrary Boolean constraints in c ∈ C is exemplified on the running
example from Figure 1b. Consider the arbitrary constraint Diesel ∧ V8 →
LeftTank ∧ RightTank. The corresponding Tbox axiom is DTruck v ¬(DDiesel u
DV8 ) t (DLeftTank u DRightTank ), where DTruck is the root of the FM.
4.3 Arbitrary model M as Tbox axioms
Given an arbitrary model M = (O, R, J·KT ), the Tbox encoding consists of the
encoding of: objects in O, relations in R, presence conditions of objects in O, the
absence of relations because of the underlying open-world assumption, and inverse
relation described in the beginning of Section 4.1. The encoding is exemplified
Verifying Contract-Based Specifications of Product Lines using DL 9
by using particular types of objects and relations but the encoding principles are
similar for all other types of objects and relations.
a) Encoding objects. For each oi ∈ O such that oTi = Guarantee, the Tbox is
complemented with axioms Doi ∈ NC , Doi v DSG , DSG ≡ ti Doi , and for
each Doi and Doj6=i , Doi u Doj v ⊥.
b) Encoding relations. For each oi ∈ O such that oTi = Guarantee and each
pair (oi , o1 ), . . . , (oi , on ) ∈ R where (oi , o1 )T = · · · = (oi , on )T = fulfills,
the Tbox is complemented with axioms Doi v unj=1 = 1 Rfulls .Doj , and
Doi v ∀Rfulls .(tnj=1 Doj ).
c) Encoding presence conditions. For each oi ∈ O labeled with a pres-
ence condition Φ(oi ), the Tbox is complemented with axioms DΦ(oi ) ∈
NC ,DΦ(oi ) v DP , and DΦ(oi ) ≡ ΦDL (oi ) where ΦDL (oi ) is the DL encoding
of the presence condition according to the same principles as for arbitrary
FM constraints.
d) Encoding the absence of relations. For each oi ∈ O such that oTi =
Guarantee and Doi v DS , where DS is the domain restriction of role Rfulls , if
there is no oj ∈ O such that (oi , oj ) ∈ R and (oi , oj )T = fulfills, the Tbox is
complemented with the axiom Doi v ¬(∃ Rfulls .DS ) where DS is the range
restriction of the role Rfulls .
e) Encoding inverse relations. Because each pair (oi , oj ) ∈ R implicitly
defines its inverse pair (oj , oi ), the relations inverse to fulfills, hasAssumption,
hasGuarantee can be constructed, and the encoding principle (b) can be used
to encode the relations represented by roles RfullBy , RaPartOf , and RgPartOf .
Using the running example, we exemplify the usage of the encoding principles.
Object FuelSensor from Figure 2b is encoded as DFuelSensor v DCA and declared
to be pairwise disjoint with each of the three remaining concepts DBMS , DCOO ,
and DICL . As an example of relation encoding, consider the pair (A1 , G1 )T =
assumptionOf whose encoding is DA1 v= 1 RassOf .DG1 and DA1 v ∀RassOf .DG1 .
Note that the reason for encoding relations using both value restrictions and
number restrictions, is because value restriction does not guarantee the existence
of the relation. As an example of a presence condition encoding, consider Φ(A2 ) =
ϕ5 = Truck ∧ V8 which is encoded as DΦ(A2 ) ≡ DTruck u DV8 . Finally, for an
example of the absence of a relation, consider assumption A1 . Because each
Assumption is a Specification, and DS which corresponds to Specification is
the domain restriction of the role Rfulls , because there is no Specification Sk
such that (A1 , Sk )T = fulfills, then the Tbox is complemented with the axiom
DA1 v ¬(∃ Rfulls .DS ) where DS is the range restriction of Rfulls .
The presence condition semantics defined in Definition 7 is preserved by the
corresponding Tbox encoding due to the following theorem.
Theorem 2. Given a presence condition ϕ expressed over features f1 , . . . , fm ,
and corresponding concepts Dϕ and Df1 , . . . , Dfm , if Dϕ ≡ ϕDL , where ϕDL is
obtained by replacing each feature fi from ϕ with Dfi , each ∧ with u, each ∨
with t, and preserving each ¬, then it holds that JϕK = DϕI .
The presence conditions semantics in Definition 7 is defined under the the closed-
world assumption, i.e. only the explicitly created product individuals p can be
10 D. Nešić and M. Nyberg
elements of JϕK. For example, there are thousands of configurations of the FLD
system and only some configurations are instantiated into product individuals
p. Consequently, JϕK can only be analyzed with respect to the created p. Given
Theorem 2 and the the open-world assumption of DL, reasoning about DϕI is
possible without asserting a single named individual in the Abox.
5 Verifying that M is a proper specification structure
This section presents the encoding of the constraints from Definition 5 and
Definition 6 as Tbox axioms. Note that it is assumed that constraint iii) from
Definition 6 is verified elsewhere.
The constraint from Definition 5 and Definition 6 can be partitioned into
two groups; the ones about presence condition, and the unrelated to presence
condition. The latter group includes constraints (i), (ii), (iv), (v) from Definition 5
and (i) and (ii) from Definition 6. The former group includes constraints (iv)-(viii)
from Definition 6. Here the encoding of a single constraint from both groups
is presented while the remaining ones can be found in [26]. An example of a
constraint unrelated to presence conditions is constraint (v)-a) from Definition 5.
Definition 5(v)-a: For each edge fulfills(Si , Sj ) if Si is a guarantee then Si is
a guarantee of a contract Ki and Sj is either an assumption Aj or the guarantee
G0 . The constraint is encoded by a concept D5(v)−a where the expression to the
left of u oprator defines the conditions on Si and the expression to right defines
conditions on Sj .
D5(v)−a ≡(∃ RgPartOf .(∃ RalcTo .(∃ Rcomp .DC 0 ))) u
(∀ Rfulls .((∃ RaPartOf .(∃ RalcTo .(∃ Rcomp .DC 0 ))) t DG0 ))
Given a model M, for each {oi , oj } ⊆ O such that oTi = Guarantee, and (oi , oj )T =
fulfills, it should be verified that the concept corresponding to Doi is subsumed
by D5(v)−a , i.e. K |= Doi v D5(v)−a . In accordance with [18], verifying that a KB
entails the above inclusion is equivalent to verifying that the KB is not satisfiable
if the Tbox is complemented with a fresh concept DFresh ≡ Doi u ¬(D5(v)−a ).
An example of a constraint related to presence condition is constraint (vii)
from Definition 6.
Definition 6(vii): For each contract Ki = (Ai , Gi ) allocated to an atomic
component Ci and W for each specification Sk such that fulfills(Sk , Ai ) it holds
that Φ(Ai ) |=C fulfills(Sk ,Ai ) Φ(Sk ). Given a model M, for each set of pairs
{(o1 , oi ), · · · , (on , oi )} ⊆ R such that oTi = Assumption, (o1 , oi )T = . . . =
(on , oi )T = fulfills, and Φ(oi ), Φ(o1 ), . . . , Φ(on ) are the corresponding presence
conditions, it should be verified that K |= DΦ(oi ) v tnj=1 DΦ(oj ) . Note that be-
cause an FM V = (F, C) is already encoded as a set of Tbox axioms, verification
that the above inclusion holds is with respect to the constraints in C. Verifying
the entailment of the above inclusion is done in the same way as for D5(v)−a .
Similarly to the constraints above, for an arbitrary model M, each condition
from Definition 5 and Definition 6 can be formulated as an inclusion axiom
Di v Dj and verified by establishing that K |= Di v Dj . Let R be a set of all
inclusion axioms required to establish that M is a proper specification structure.
Verifying Contract-Based Specifications of Product Lines using DL 11
Theorem 3. Given a model M, a corresponding knowledge base K = (T , A),
and the set R, if ∀r ∈ R.K |= r, then M is a proper specification structure.
5.1 Implementation
In order to validate the presented encoding, the running example was manually
implemented as an OWL ontology using the Protege [35] tool and HermiT [33]
reasoner was used to perform the reasoning. The resulting ontology was SRIQ
DL and it contained 463 axioms with 45 additional axioms needed to verify
if the running example is a proper specification structure. As can be verified
from Figure 2b, the analysis showed that Φ(A4 ) and Φ(G4 ) do not entail Φ(ICL),
thus violating constraint (v) of Def. 6, i.e. the running example is not a proper
specification structure. The resulting ontology is available online3 .
6 Conclusion
Compliance with standards regulating the development of critical systems is often
shown using assurance cases. Assurance cases are comprised of two main parts, the
arguments about the intended system properties and the evidences which support
the arguments. As discussed in Section 1, Contract-Based Specification (CBS)
frameworks have shown to be useful as the basis of assurance case arguments but
only if they conform to a number of constraints. The present paper has presented
a DL-based method for the verification of these constraints against an arbitrary
CBS model of a product line of systems. Although other technologies, besides
DL, can be used to perform such verifications, DL was used because DL is the
foundation of OWL which is part of the Semantic Web stack and Semantic Web
is a promising approach for cleaning, integrating, and enabling uniform access to
the evidences required for an assurance case. Because some constraints require
verification of propositional entailment it was not possible to encode a CBS model
as a set of Abox assertions, and the constraints to which a CBS model must
conform to as a set of Tbox axioms. Instead, both the CBS model and the CBS
constraints were encoded as Tbox axioms and a new DL concept was added for
each CBS model-element that was in the scope of a constraint. In other words,
the number of additional DL concepts needed for the verification of a CBS model
is linear in the size of the CBS model. A drawback of using DL and the underlying
open-world assumption was the need to explicitly declare negative facts about the
given CBS model, thus incurring an overhead compared to technologies working
under the closed-world assumption. Still, each of the several types of verifications
was possible to encode as the Tbox satisfiability problem and routinely checked
by an off-the-shelf reasoner. Furthermore, the presented DL semantics of PL
concepts feature, product configuration, and presence condition naturally captures
the intuition that each of these concepts represents subsets of the set of all possible
product individuals. Future work includes applying the presented method on a
CBS model of a full-scale FLD system PL.
3
https://goo.gl/8G5Wec
12 D. Nešić and M. Nyberg
References
1. Goal structuring notation community standard version 2 (Jan 2018),
https://scsc.uk/r141B:1?t=1
2. Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-oriented software product
lines. Springer-Verlag, Berlin-Heidelberg, Germany (2016)
3. Apel, S., Kästner, C.: An overview of feature-oriented software development (2009)
4. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.
(eds.): The Description Logic Handbook: Theory, Implementation, and Applications.
Cambridge University Press (2003)
5. Bansal, S.K.: Towards a semantic extract-transform-load (etl) framework for big
data integration. In: 2014 IEEE International Congress on Big Data. pp. 522–529
(2014)
6. Batory, D.: Feature models, grammars, and propositional formulas. In: International
Conference on Software Product Lines. pp. 7–20 (2005)
7. Benavides, D., Segura, S., Ruiz Cortés, A.: Automated analysis of feature models
20 years later: A literature review. Information Systems 35(6) (2010)
8. Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinke-
meier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T.A., Larsen, K.G.:
Contracts for system design. Foundations and Trends® in Electronic Design Au-
tomation (2-3), 124–400 (2018)
9. Bizer, C., Heath, T., Berners-Lee, T.: Linked data: The story so far. In: Semantic
services, interoperability and web applications: emerging concepts, pp. 205–227.
IGI Global (2011)
10. Braun, G., Pol’la, M., Buccella, A., Cecchi, L., Fillottrani, P., Cechich, A.: A dl
semantics for reasoning over ovm-based variability models. In: Description Logic
workshop (2017)
11. Caillaud, B.: A modal interface compositional analysis library (Oct 2011),
www.irisa.fr/s4/tools/mica
12. Czarnecki, K., Wasowski, A.: Feature diagrams and logics: There and back again.
In: Proceedings of the International Software Product Line Conference. pp. 23–34.
SPLC ’07 (2007)
13. Dabney, J.B., Harman, T.L.: Mastering simulink. Pearson (2004)
14. Fan, S., Zhang, N.: Feature model based on description logics. In: Gabrys, B.,
Howlett, R.J., Jain, L.C. (eds.) Knowledge-Based Intelligent Information and
Engineering Systems (2006)
15. Gunes, V., Peter, S., Givargis, T., Vahid, F.: A survey on concepts, applications, and
challenges in cyber-physical systems. KSII Transactions on Internet & Information
Systems 8(12) (2014)
16. Halin, A., Nuttinck, A., Acher, M., Devroey, X., Perrouin, G., Baudry, B.: Test
them all, is it worth it? Assessing configuration sampling on the JHipster Web
development stack. Empirical Software Engineering (Jul 2018)
17. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible sroiq. In: Proceedings
of the International Conference on Principles of Knowledge Representation and
Reasoning ’06. pp. 57–67 (2006)
18. Horrocks, I., Patel-Schneider, P.: Reducing owl entailment to description logic
satisfiability. Web Semantics: Science, Services and Agents on the World Wide Web
1(4), 345 – 357 (2004)
19. ISO61508: Functional Safety. standard, The International Electrotechnical Com-
mission, Geneva, CH (2010)
Verifying Contract-Based Specifications of Product Lines using DL 13
20. ISO26262: Road vehicles - Functional safety. standard, International Organization
for Standardization, Geneva, CH (2011)
21. Kastner, C., Thum, T., Saake, G., Feigenspan, J., Leich, T., Wielgorz, F., Apel,
S.: Featureide: A tool framework for feature-oriented software development. In:
Proceedings of the 31st International Conference on Software Engineering. pp.
611–614 (2009)
22. Liu, H., Li, Q., Gu, N., Liu, A.: Modeling and reasoning about semantic web services
contract using description logic. In: 2008 The Ninth International Conference on
Web-Age Information Management. pp. 179–186 (July 2008)
23. McGuinness, D.L., Van Harmelen, F., et al.: Owl web ontology language overview.
W3C recommendation 10(10) (2004)
24. Mukelabai, M., Nešić, D., Maro, S., Berger, T., Steghöfer, J.P.: Tackling combi-
natorial explosion:a study of industrial needs and practices for analyzing highly
configurable systems. In: Proceedings of ASE’18 (2018)
25. Nešić, D., Nyberg, M.: Modeling product-line legacy assets using multi-level theory.
In: Proceedings of International Systems and Software Product Lines Conference
’17 - Volume B. pp. 89–96 (2017)
26. Nešić, D., Nyberg, M.: Contract-based specification and description-logic-based vali-
dation of product lines. Technical report, Royal Institute of Technology, Stockholm,
Sweden (2018)
27. Nešić, D., Nyberg, M.: Applying multi level modeling to data integration in product
line engineering. In: Proceedings MODELS Satelite events: International Workshop
on Multi-Level Modeling ’17. pp. 235–242 (2017)
28. Noorian, M., Ensan, A., Bagheri, E., Boley, H., Biletskiy, Y.: Feature model
debugging based on description logic reasoning. In: DMS (2011)
29. Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering.
Foundations, Principles, and Techniques. Springer (2005)
30. Quinton, S., Graf, S.: Contract-based verification of hierarchical systems of compo-
nents. In: Proceedings IEEE International Conference on Software Engineering and
Formal Methods ’08. pp. 377–381 (2008)
31. Ryssel, U., Ploennigs, J., Kabitzsch, K.: Reasoning of feature models from derived
features. SIGPLAN Not. 48(3), 21–30 (Sep 2012)
32. Shadbolt, N., Berners-Lee, T., Hall, W.: The semantic web revisited. IEEE Intelligent
Systems pp. 96–101 (2006)
33. Shearer, R., Motik, B., Horrocks, I.: Hermit: A highly-efficient owl reasoner. In:
OWLED. vol. 432, p. 91 (2008)
34. Sljivo, I., Gallina, B., Carlson, J., Hansson, H.: Generation of safety case argument-
fragments from safety contracts. In: Proceedings International Conference on Com-
puter Safety, Reliability, and Security ’14. pp. 170–185 (2014)
35. Stanford Center for Biomedical Informatics Research: Protege ontology editor
(2016), https://protege.stanford.edu/
36. Wang, H.H., Li, Y.F., Sun, J., Zhang, H., Pan, J.: Verifying feature models using
owl. Web Semantics 5(2), 117–129
37. Westman, J., Nyberg, M.: Conditions of contracts for separating responsibilities
in heterogeneous systems. Formal Methods in System Design 52(2), 147–192 (Apr
2018)
38. Wozniak, L., Clements, P.: How automotive engineering is taking product line
engineering to the extreme. In: SPLC ’15 (2015)
39. Zou, J., Wang, Y., Lin, K.J.: A formal service contract model for accountable saas
and cloud services. In: 2010 IEEE International Conference on Services Computing.
pp. 73–80 (July 2010)