Verifying Contract-Based Speci cations of Product Lines using Description Logic

Abstract

The complexity of critical systems is constantly increasing and if developed as Product Lines (PLs), the number of possible system con guration can be huge. Consequently, assuring system properties such as safety or security is increasingly di cult. Assurance cases are used often to argue that a system is safe or secure and Contract-Based Speci cation models are a promising foundation for assurance case argumentation. This paper de nes a method for Description Logic (DL) based veri cation 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 veri cation of these constraints can be reduced to satis ability veri cation 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 o -the-shelf reasoner was used to verify if the CBS model is well-formed.

-

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 con gurations is possible. As a consequence, assuring that the complete PL satis es properties like safety or security is increasingly di cult and in the case of a very high number of con gurations 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 de ned application in a de ned environment" [ 1 ]. Developing the assurance case argumentationstructure and identifying the appropriate evidences are both di cult tasks. The required "body of evidence" are concrete engineering artifacts, such as results of safety analyses, speci cations, test cases etc. These are usually maintained and evolved by di erent tools, which in an enterprise setting often leads to inconsistencies among these artifacts. As argued in [ 5, 27 ], Semantic Web [ 32 ], 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.

Di culties 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 di erent 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 speci cation, design, and input for veri cation of complex, heterogeneous PLs is the Contract-Based Speci cation (CBS) framework [ 8, 30, 37 ] and its PLE extension [ 26 ]. As brie y 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 veri ed 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 veri cation 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 e ort of automating the prevailingly manual process of assurance case construction. The results show that using DL for the veri cation 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 di erent 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 ne-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 o -the-shelf reasoners to analyze the possible product con gurations 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 o -the-shelf reasoners to detect similar product con guration 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 of the FM encoding is to support the analysis of CBS models, the DL semantics of FM constructs is di erent and the encoding is more compact.

Paper Structure. Section 2 summarizes the concepts underlying PLE, CBS and the constraints to be veri ed against an arbitrary CBS model. Section 3 de nes 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 exempli es how an arbitrary CBS model can be veri ed against the de ned 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 con guration is selected, and the set of artifacts that implement the selected product con guration 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

De nition 1 (Feature Model). A feature model V is a pair V = (F ; C) where F = ff1; : : : ; fng is a set of features and C is a set of Boolean constraints over the features in F .

FMs de ne 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.

De nition 2 (Product Con guration). Given a feature model V = (F ; C), a product con guration, denoted as PC , is a set of feature value-assignments such that each fi 2 F is assigned with a value true or false. A product con guration for which each Boolean constraint in C evaluates to true is valid.

A product con guration represents, in terms of features, all individual systems that are identically con gured. As discussed previously, the feature representation is mapped to the representation in terms of concrete artifacts by labeling the artifacts with presence conditions. (a) Used FM graphical syntax. (b) FM running example.

2.2 Contract-Based Speci cation and Design

The basic concepts of CBS are shown in Figure 2a. Given these, the central concept of a Contract is de ned as following.

De nition 4 (Contract). A Contract K is an ordered pair of speci cations, 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 satis es a contract K = (A; G) if for each component C0 such that implements(C0; A), the component C00 is such that implements(C00; G) where composedOf(C00; C0) and composedOf(C00; 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 Speci cation 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 Speci cation S - Requirement on C behaviour implements(C; S) - C behaviour conforms to S ful lls(Si; Sj) - 8C:implements(C; Si) !

implements(C; Sj) composedOf(C; C1) - C1 comprises C aDetailed descriptions can be found in [ 26 ].

(a) Basic CBS concepts (b) FLD system running example.

The composite component FLD is composed of atomic components FuelSensor, COO, short for COOrdinator, BMS, short for Body Management System, and ICL, short for Instrumentation CLuster. Relations ful lls 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 speci cation 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 ful lls G0. The dashed border of BMS and COO indicates that these components are not present in each product con guration, i.e. COO is responsible for volts to liters conversions in product con gurations with diesel fuel, while BMS, performs the same conversion in product con gurations with gas fuel. In other words, the CBS model in Figure 2b de nes 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 speci cation structure.

De nition 5 (Speci cation 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 K0 = (A0; G0) allocated to the composite component C0, which is composed of atomic components Ci, an edge-labeled directed graph D = (N ; E) is a speci cation structure if: i) each node n 2 N is either an assumption Ai or A0 or a guarantee Gi or G0, ii) each edge e = (ni; nj) 2 E corresponds to either a single assumptionOf(Si; Sj) or a single ful lls(Si; Sj) relation, iii) for each edge e = (ni; nj) 2 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 ful lls(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.

De nition 5 allows circular speci cation structures, or presence conditions of an assumption A and a guarantee G of a contract (A; G) such that in some product con gurations A and G do not simultaneously apply. To avoid such cases, a proper speci cation structure is de ned. The entailment between presence conditions 'i and 'j is denoted as 'i j=C 'j as a short hand for (C; 'i) j= '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 j=C '1. De nition 6 (Proper Speci cation Structure). Given a feature model V = (F ; C), a speci cation structure is proper if: i) for each assumption Ai of a contract Ki, there exists a speci cation Sk such that ful lls(Sk; Ai), where Sk is either A0 or Gi, ii) there exists a guarantee Gi such that ful lls(Gi; G0), iii) the graph of D is acyclic, iv) for each contract (Ai; Gi), it holds that (Ai) j=C (Gi) and (Gi) j=C (Ai), v) for each contract (Ai; Gi) allocated to a component Ci it holds that (Ai) j=C (Ci) and (Gi) j=C (Ci), vi) for the composite component C0 composed of atomic components Ci, for each

Ci it holds that (Ci) j=C (C0), vii) for each contract Ki = (Ai; Gi) allocated to an atomic component Ci and for each speci cation Sk such that ful lls(Sk; Ai) it holds that (Ai) j=C Wful lls(Sk;Ai) (Sk), viii) for the contract K0 = (A0; G0) allocated to the composite component C0 and for each guarantee Gi of a contract Ci such that ful lls(Gi; G0) it holds that (G0) j=C Wful lls(Gi;G0) (Gi).

The following theorem presents the key compositional idea of the CBS [ 26 ]. Note that in the following theorem, symbol j= means entailment between Si; Sj irregardless of the formalisms used to express Si and Sj .

Theorem 1. Given a feature model V, and a speci cation structure D, if i) D is proper, ii) for each relation ful lls(Si; Sj ), it holds that Si j= Sj , iii) each atomic component Ci satis es the contract allocated to it, then, for each valid product con guration PCi , the composite component C0 satisifes the contract K0.

Less formally, if a CBS model of a PL is a proper speci cation structure, and if each pair of speci cations in ful lls relation entail each other, then by verifying that each component of each PL product con guration satis es the contract allocated to it, it can be inferred that each product con guration satis es the contract allocated to it. The remainder of the paper shows how to verify that an arbitrary CBS model, is a proper speci cation 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 speci cations structure, it is necessary to de ne 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 in nite number of product individuals p can be created by instantiating the PL design. From this it follows that each product con guration 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.

Let Con g be a function which given a product individual p returns its product con guration PC . Moreover, let Eval be a function that takes a presence condition ' and a product con guration PC and returns the value of ' for the given PC .

De nition 7 (Presence condition semantics). The semantics of a presence

condition ', denoted as J'K, is J'K = fpj Eval('; Con g(p)) = trueg.

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 fG1; A2g O, (G1; A2) 2 R, and G1T = Speci cation, A1T = Speci cation, (G1; A1)T = ful lls.

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 de ned in [ 4 ]. 4.1

General CBS entities and relations as Tbox axioms

Before de ning 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 speci cation structure and speci cations, denoted hasSpeci cation(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 relation 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 De nition 5 and De nition 6 will require these roles.

According to the discussion in Section 3, the Tbox is complemented with the concept DP 2 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 speci cations 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, De nition 4 and condition (iii) from De nition 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 De nition 4, and axioms 9 RassOf :Self v ? and 9 Rfulls :Self v ? correspond to condition (iii) of De nition 5. The semantics of the construct 9R:Self is de ned in [ 17 ].

4.2 Arbitrary FM as Tbox axioms

In order to verify conditions (iv)-(viii) from De nition 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 con gurations. The present paper encodes the FM di erently and the semantics of each feature f is a set of product individuals whose product con guration PC is such that (f = true) 2 PC . Consequently, the semantics of concepts based on features, e.g. presence conditions or product con gurations, 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.

Encoding arbitrary Boolean constraints in c 2 C is exempli ed 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.

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 exempli ed 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 2 O such that oiT = Guarantee, the Tbox is complemented with axioms Doi 2 NC , Doi v DSG , DSG tiDoi , and for each Doi and Doj6=i , Doi u Doj v ?. b) Encoding relations. For each oi 2 O such that oiT = Guarantee and each pair (oi; o1); : : : ; (oi; on) 2 R where (oi; o1)T = = (oi; on)T = ful lls, n the Tbox is complemented with axioms Doi v uj=1 = 1 Rfulls :Doj , and n

Doi v 8Rfulls :(tj=1Doj ).

c) Encoding presence conditions. For each oi 2 O labeled with a pres

ence condition (oi), the Tbox is complemented with axioms D (oi) 2 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 2 O such that oiT = Guarantee and Doi v DS, where DS is the domain restriction of role Rfulls , if there is no oj 2 O such that (oi; oj) 2 R and (oi; oj)T = ful lls, the Tbox is complemented with the axiom Doi v :(9 Rfulls :DS) where DS is the range restriction of the role Rfulls . e) Encoding inverse relations. Because each pair (oi; oj) 2 R implicitly de nes its inverse pair (oj; oi), the relations inverse to ful lls, 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 8RassOf :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 Speci cation, and DS which corresponds to Speci cation is the domain restriction of the role Rfulls , because there is no Speci cation Sk such that (A1; Sk)T = ful lls, then the Tbox is complemented with the axiom DA1 v :(9 Rfulls :DS) where DS is the range restriction of Rfulls .

The presence condition semantics de ned in De nition 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 De nition 7 is de ned under the the closedworld assumption, i.e. only the explicitly created product individuals p can be elements of J'K. For example, there are thousands of con gurations of the FLD system and only some con gurations 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 speci cation structure This section presents the encoding of the constraints from De nition 5 and De nition 6 as Tbox axioms. Note that it is assumed that constraint iii) from De nition 6 is veri ed elsewhere.

The constraint from De nition 5 and De nition 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 De nition 5 and (i) and (ii) from De nition 6. The former group includes constraints (iv)-(viii) from De nition 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 De nition 5.

De nition 5(v)-a: For each edge ful lls(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 de nes the conditions on Si and the expression to right de nes conditions on Sj.

D5(v) a (9 RgPartOf :(9 RalcTo:(9 Rcomp:DC0 ))) u

(8 Rfulls :((9 RaPartOf :(9 RalcTo:(9 Rcomp:DC0 ))) t DG0 )) Given a model M, for each foi; ojg O such that oiT = Guarantee, and (oi; oj)T = ful lls, it should be veri ed that the concept corresponding to Doi is subsumed by D5(v) a, i.e. K j= 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 satis able 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 De nition 6.

De nition 6(vii): For each contract Ki = (Ai; Gi) allocated to an atomic component Ci and for each speci cation Sk such that ful lls(Sk; Ai) it holds that (Ai) j=C Wful lls(Sk;Ai) (Sk). Given a model M, for each set of pairs f(o1; oi); ; (on; oi)g R such that oiT = Assumption, (o1; oi)T = : : : = (on; oi)T = ful lls, and (oi); (o1); : : : ; (on) are the corresponding presence n conditions, it should be veri ed that K j= D (oi) v tj=1D (oj). Note that because an FM V = (F ; C) is already encoded as a set of Tbox axioms, veri cation 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 De nition 5 and De nition 6 can be formulated as an inclusion axiom Di v Dj and veri ed by establishing that K j= Di v Dj. Let R be a set of all inclusion axioms required to establish that M is a proper speci cation structure. Theorem 3. Given a model M, a corresponding knowledge base K = (T ; A), and the set R, if 8r 2 R:K j= r, then M is a proper speci cation 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 speci cation structure. As can be veri ed 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 speci cation 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 Speci cation (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 veri cation 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 veri cations, 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 veri cation 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 veri cation 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 veri cations was possible to encode as the Tbox satis ability problem and routinely checked by an o -the-shelf reasoner. Furthermore, the presented DL semantics of PL concepts feature, product con guration, 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

References

1. Goal structuring notation community standard version 2 ( Jan 2018 ), https://scsc.uk/r141B:1?t= 1

2. Apel , S. , Batory , D. , Kastner, C. , Saake , G.: Feature-oriented software product lines . Springer-Verlag, Berlin-Heidelberg, Germany ( 2016 )

3. Apel , S. , Kastner, 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 Cortes , 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. , Reinkemeier , P. , Sangiovanni-Vincentelli , A. , Damm , W. , Henzinger , T.A. , Larsen , K.G. : Contracts for system design . Foundations and Trends® in Electronic Design Automation (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 con guration 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 satis ability . Web Semantics: Science, Services and Agents on the World Wide Web 1 ( 4 ), 345 { 357 ( 2004 )

19. ISO61508: Functional Safety. standard, The International Electrotechnical Commission , Geneva, CH ( 2010 )

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. , Nesic , D. , Maro , S. , Berger , T. , Steghofer, J.P. : Tackling combinatorial explosion:a study of industrial needs and practices for analyzing highly con gurable systems . In: Proceedings of ASE'18 ( 2018 )

25. Nesic , 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. Nesic , D. , Nyberg , M. : Contract-based speci cation and description-logic-based validation of product lines . Technical report , Royal Institute of Technology, Stockholm, Sweden ( 2018 )

27. Nesic , 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. , Bockle, G., van der Linden , F.J.: Software Product Line Engineering . Foundations, Principles, and Techniques. Springer ( 2005 )

30. Quinton , S. , Graf , S. : Contract-based veri cation of hierarchical systems of components . 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-e cient owl reasoner . In: OWLED . vol. 432 , p. 91 ( 2008 )

34. Sljivo , I. , Gallina , B. , Carlson , J. , Hansson , H.: Generation of safety case argumentfragments from safety contracts . In: Proceedings International Conference on Computer 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 )