=Paper=
{{Paper
|id=Vol-2019/modcomp_4
|storemode=property
|title=OCL Framework to Verify Extra-Functional Properties in Component and Connector Models
|pdfUrl=https://ceur-ws.org/Vol-2019/modcomp_4.pdf
|volume=Vol-2019
|authors=Shahar Maoz,Ferdinand Mehlan,Jan Oliver Ringert,Bernhard Rumpe,Michael von Wenckstern
|dblpUrl=https://dblp.org/rec/conf/models/MaozMRRW17
}}
==OCL Framework to Verify Extra-Functional Properties in Component and Connector Models==
https://ceur-ws.org/Vol-2019/modcomp_4.pdf
OCL Framework to Verify Extra-Functional
Properties in Component and Connector Models
Shahar Maoz1 , Ferdinand Mehlan2 , Jan Oliver Ringert1 , Bernhard Rumpe2 , and Michael von Wenckstern2
1
School of Computer Science, Tel Aviv University, Israel http://www.cs.tau.ac.il
2
Software Engineering, RWTH Aachen University, Germany http://www.se-rwth.de
Abstract—We present an OCL framework and tool for the de- for the definition and analysis of EFP consistency of C&C
scription and verification of consistency rules of extra-functional models.
properties (EFPs) in component and connector (C&C) models. Our first contribution is a C&C-specific extension of
The framework is based on our previously defined structure of
EFP consistency rules using selection, aggregation, and compar- OCL. The extension allows the definition of C&C consistency
ison operators, and provides C&C specific OCL functions and constraints based on clean mathematical C&C definitions; all
configurations that allow engineers to succinctly express EFP implementation specific details, such as more complex types
consistency rules for C&C models. Further, the extension of from the meta-model or abstract-syntax representations are
OCL is twofold. First, constraints may contain C&C specific ex- abstracted away by providing C&C specific OCL configura-
pressions and second, expressions natively support measurement
units as required in specifications of EFPs. We have extended tions and powerful type-inference mechanisms when checking
the OCL verification process to support the novel extensions consistency.
and to automatically generate meaningful positive and negative Our second contribution extends OCL with support
witnesses for consistency and inconsistency. We implemented for measurement units and an automatic mechanism to
the approach within the MontiCore framework for the C&C produce witnesses for EFP consistency checking results.
modeling language MontiArc. Initial evaluation shows that it is
expressive and scales to large, industrial sized C&C models. First, many EFPs, describing physical properties of C&C
models, e.g., WCET, power consumption, or memory usage,
I. I NTRODUCTION contain physical units, e.g., seconds, Watts, or sizes. Thus,
to enable domain experts define EFP consistency rules, a
Component and connector (C&C) models are used in many constraint language for EFPs naturally should support auto-
application domains of software engineering, from cyber- matic unit comparison and conversion . Second, our previously
physical and embedded systems to web services and enterprise defined mathematical framework [12] structures the definition
applications. The structure of C&C models consists of com- of consistency rules. This general structure allows to automat-
ponents at different containment levels, their typed interaction ically generate positive and negative witnesses for consistency
points, and connectors between them [13]. In addition to checking results. These witnesses intuitively demonstrate the
functional properties, extra-functional properties (EFPs) play reasons for consistency or inconsistency of a C&C model.
an important role in the development of C&C models [6], Our third contribution is an initial evaluation of
[19]–[21]. Important examples of EFPs include worst-case- checking EFP consistency of an industrial sized C&C
execution-time (WCET), memory and power consumption, model. Specifically, we used our tool to verify four selected
security properties, and traceability [1], [16], [18]. consistency rules on an industrial sized Autonomous Driver
Recently, we have presented a non-invasive technique for Assistance System (ADAS) model. The ADAS model consists
adding EFPs to C&C models by means of tagging lan- of about 1,400 components and 4,500 ports, and 2,800 tagged
guages [12]. Importantly, this technique requires no changes EFP values. Our examples and evaluation show that (i) our
to the meta-model of the C&C language. In addition, we OCL based approached is expressive enough for defining
have suggested a generic structure for EFP consistency rules complex consistency constraints, and (ii) that the performance
based on selection, aggregation, and comparison operators. of our implementation for checking these consistency rules
Conceptually, a consistency rule states for a C&C element scales to large models.
and an EFP whether the EFP value is consistent with the EFP In the next section we present a running example. Sect. III
values of other C&C elements. Technically, consistency rules gives background on C&C models and consistency rules of
are constraints that are satisfied iff the EFP value is consistent. EFPs. Sect. IV and Sect. V present our OCL framework and
Consistency is determined by comparison to aggregated EFP example constraints, Sect. VI presents the implementation, and
values of related C&C elements as defined by the selection, Sect. VII presents a case study in which the framework is used.
aggregation, and comparison operators of consistency rules. Sect. VIII present related work, and Sect. IX concludes.
In this paper we are interested in the concrete formalization
of EFP consistency rules and in their automated analysis. II. RUNNING E XAMPLE
We propose to leverage the popular and expressive Object Consider the sensor block of a weather balloon system as
Constraint Language [25] (OCL) and its analysis capabilities shown in Fig. 1 (for textual syntax, see Fig. 2). The sensor
extra-functional properties 1 component WBalloonSens { MA
component type C&C 2 ports in Byte[] controlSig, top component definition
is instantiated once with
3 out Byte[] dataSave, instance name wBalloonSens
WBalloonSens power=5W, wcet=2s 4 out Byte[] dataAntenna;
wBalloonSens 5 component Controller controller;
instance name Controller
power=10mW,
6 component GPS gps1, gps2;
wcet=50ms 7 component Temperature temp;
controlSig
Temp power=400mW, wcet=500ms controller 8 ...
connect controller.antenna -> dataAntenna;
dataSave
9
temp power=400mW, wcet=500ms
10 connect gps1.loc -> controller.loc1; }
GPS power=2500mW, wcet=1s Fig. 2: Definitions of WBalloonSens from Fig. 1
gps1 power=2W, wcet=950ms
dataAntenna
GPS power=2500mW, wcet=1s III. P RELIMINARIES
gps2 power=2500mW, wcet=750ms
We provide background on C&C models, extra-functional
properties, and their consistency rules.
Fig. 1: Excerpt from the C&C model of the Weather Balloon Sensor System A. Component and Connector Models
Component and connector models describe components,
their points of interaction, and their hierarchical composition.
We repeat a definition of C&C models as, e.g., given in [11],
block of component type WBalloonSens consists of various in Def. 1, which represents the essence of component mod-
components: a temperature sensor (component instance temp els [13] as formalized by ADLs ACME [4], AADL [3], and
of component type Temp), two GPS sensors (component MontiArc [7], or in tools AutoFOCUS [8] and Simulink [24].
instances gps1 and gps2 of component type GPS), and a Definition 1 (Component and Connector model [11]): A
controller (component instance controller of component C&C model is a structure cncm = hCmps, Ports, Cons,
type Controller). The controller periodically pushes sensor Types, subs, ports, typei where
data to another system in order to save it. The position of the
• Cmps is a set of named components, cmp ∈ Cmps has a
balloon is important for recovery after landing. Position data
set of ports ports(cmp) ⊆ Ports and a (possibly empty)
from GPS is pushed to an antenna system, which relays the
set of immediate subcomponents subs(cmp) ⊂ Cmps,
position to ground control.
• Ports = InPorts ] OutPorts is a disjoint union of input
One EFP in our running example is power consumption (tag and output ports where each port p ∈ Ports has a name,
power). The component types and the component instances a type type(p) ∈ Types, and belongs to exactly one
in Fig. 1 are tagged with estimated power consumption, e.g., component p ∈ ports(cmp),
the component type GPS is tagged with power=2500mW • Cons is a set of directed connectors con ∈ Cons, each
and its component instance gps1 is tagged with power=2W. of which connects two ports con.src, con.tgt ∈ Ports of
The weather balloon will be running on a limited power the same type, which belong to two sibling components
supply and power consumption has to be budgeted carefully. or to a parent component and one of its immediate
Hence, the sensor block is required to consume at most 5W subcomponents, and
(see power property of component type WBalloonSens • Types is a finite set of type names.
in Fig. 1). Based on this extra-functional property of the C&C models from Def. 1 are well-formed iff no component
parent component requirements for subcomponent types are is its own (transitive) subcomponent and has at most one direct
added: Temp consumes at most 400mW , the GPS sensors parent and subcomponents are connected legally (see [11] and
GPS 2500mW each, and the controller 10mW . [17] for complete definitions).
However, the declaration of power consumption EFPs While some formalisms directly express C&C models, e.g.,
in this model is inconsistent. The subcomponents require [8], [24], others provide C&C type definitions and their
5410mW when only 5W are defined by component type instantiation to define C&C models, e.g., [3], [7].
WBalloonSens (note that it would be consistent when Definition 2 (Component Type Definition [12]): A com-
taking the component instances and not types into account, ponent type definition is a structure ct = hcType, CPorts,
which together consume 4910mW ). CSubs, CConsi ∈ CTDefs where
• cType uniquely identifies the component type,
Another EFP in our running example is the worst-case-
• CPorts is a set of input and output port definitions where
execution-time (WCET, tag wcet) of components. As we as-
each port p ∈ CPorts has a name and a type,
sume independent execution of all components and the WCET
• CSubs ⊂ N ame × CTDefs is a set of named subcom-
of each subcomponent is less than the WCET of component
ponent declarations, and
type WBalloonSens, the WCET EFPs are consistent.
• CCons is a set of directed connector definitions con ∈
Engineers can easily add EFP tags and EFP consistency CCons, each of which connects two port definitions
rules as OCL constraints, which our tool automatically verifies. con.src, con.tgt of the same type, which belong to two
sibling subcomponent declarations or to a component 2) Composition Consistency: Composition consistency
type definition and one of its subcomponent declarations. checks whether the EFPs of C&C model elements are con-
A component type t ∈ CTDefs is instantiated to a C&C sistent across their composition. The following example rules
model by creating a component for c with subcomponents, address consistency at the type level. Similar rules can be
that are instances of t.CSubs with connectors according defined at the instance level.
to t.CCons. For a more detailed definition including well- Rule 3 (CompPower [12]): The combined power consump-
formedness rules and instantiation see [17]. For an instantiated tion of all subcomponents is at most the power consumption
cmp ∈ Cmps the function CType(cmp) returns the corre- of the composed component:
sponding component type. • checks: tag power of ct ∈ CTDefs
• selection: S := ct.CSubs
B. Consistency of EFPs in C&C Models • aggregation: v :=
P
sct.power
It is important to note that the consistency of an EFP value (name,sct)∈S
may depend on multiple other C&C model elements, their • comparison: v ≤ ct.power
relations, and their EFP values. Some advanced examples of Rule 4 (ASIL): The ASIL (Automotive Safety Integrity
consistency relate to component instantiation and composition Level) of all subcomponents must be higher or equal than
in C&C models. In addition, consistency may be very specific the ASIL of the composed component:
to the EFP type, e.g., checking consistency of WCET values • checks: tag asil of cmp ∈ Cmps
is different from checking memory consumption. • selection: S := cmp.subs
To address the challenge of ensuring consistency of EFP 1
• aggregation: v := min number(sc.asil)
sc∈S
values, in a previous paper [12] we defined a general structure • comparison: v ≥ number(cmp.asil)
of EFP consistency rules shown in Def. 3. First, each rule
Rule 5 (WCET Single Core): The WCET of a component
defines what EFP value of which kind of C&C model element
instance is at most the WCET of its subcomponent instances.
it checks. Second, the rule specifies how to select relevant
• checks: tag wcet of cmp ∈ Cmps
C&C model elements for the check. Third, the rule defines
• selection: S := cmp.subs
how to aggregate tagged values over the selected elements. P
• aggregation: v := sc.wcet
Finally, the aggregated value is compared to the value of the sc∈S
checked element, to determine its consistency. • comparison: v ≤ cmp.wcet
Definition 3 (EFP Value Consistency Rule [12]): A consis- Rule 6 (WCET Multi Core): The WCET of a component
tency rule is a structure consisting of: instance is at most the maximum of the WCET of parallel
checks name of tag and element checked by rule; executable direct subcomponent paths.
selection selects relevant C&C elements to check consistency; • checks: tag wcet of cmp ∈ Cmps
aggregation aggregates values of selected elements; and • selection: S := directSubCmpP aths(cmp)
2
comparison compares values to decide consistency.
P
• aggregation: v := max elem.wcet
path∈S elem∈path
The next two subsections illustrate some examples on con-
• comparison: v ≤ cmp.wcet
sistency definition rules according to Def. 3; more examples
are available in [12]. Sect. III-B1 presents rules for the Note that our framework does not limit the selection, ag-
consistency of EFP values in the context of component type gregation, and comparison operators in any way. Our previous
instantiation. Sect. III-B2 presents rules in the context of paper [12] contains more examples with different and more
composition. complicated operators.
1) Instantiation Consistency: Instantiation consistency IV. OCL F RAMEWORK FOR C&C M ODELS
checks whether the EFPs of component instances are consis-
This section presents our first contribution: a C&C-specific
tent to the EFPs of their component type definitions.
extension of OCL.
Rule 1 (InstPower [12]): The power consumption of an
We start with an example. The top part in Fig. 3 presents
instance is at most the power consumption of its type:
an OCL invariant expressing that the source and target
• checks: tag power of cmp ∈ Cmps
ports of a connector have the same data type (l. 3). Typi-
• selection: t := CType(cmp) ∈ CTDefs
cally, OCL constraints are written against a concrete meta-
• aggregation: v := cmp.power
model; this, however, makes the OCL constraints depen-
• comparison: v ≤ t.power
dent on a specific language implementation. As an ex-
Rule 2 (InstCertificates): The certificates of component ample, our C&C language implementation MontiArc pro-
instances must be at most the certificates common to all ports vides references to all connectors in a C&C model by:
of the component: List connectors = global-
• checks: tag cert of cmp ∈ Cmps Scope.resolve(ConnectorSymbol.KIND) [14]. A
• selection: P := cmp.ports
T 1 QM = 0, ASIL A = 1, ASIL B = 2, ASIL C = 3, ASIL D = 4
• aggregation: v := p∈P p.cert 2 directSubCmpPaths(cmp) computes the set of all paths from a
• comparison: v ⊇ cmp.cert subcomponent of cmp to an output port of cmp.
1 import CnCExt; 1 import CnCExt; OCL
OCL
2 ocl ruleConnectorSamePortType { 2 import EFPExt;
3 ocl ruleInstPower {
3 context Con con inv: con.src.type == con.tgt.type }
4 context Cmp cmp inv: // checks: ∈
CnCExt.conf 5 let
5 import de.monticore.lang.montiarc._symboltable.*; 6 selectedValue = cmp.CType; // selection: ≔ ( )∈
6 import static de. … .montiarc.helper.GraphFunctions.*;
7 aggregatedValue = max(cmp.power, 0W);// aggregation: ≔ .
7 rewrite "Con" -> "ConnectorSymbol"; 8 in consider maximum value of the power tags, and “0W” if power tag is missing
8 rewrite "src" -> "getSourcePort()"; 9 aggregatedValue <=
// comparison: ≤ .
9 rewrite "tgt" -> "getTargetPort()"; 10 min(selectedValue.power,+ooW); }
10 rewrite "type" -> "getType()";
11 …
Fig. 4: OCL constraint for instantiation consistency of EFP power (Rule 1)
Fig. 3: Top: OCL Expression for same port type of connected ports. Bottom:
1 // positive witness for checking: shows if positive or negative witness
Excerpt of C&C MontiArc specific configuration file. 2 // ocl "ruleInstPower.ocl" on model "WBalloonSens.ma"
3 // aggregated value in model: 2 W
aggregated values,
useful for
4 component WBalloonSens {
complex
5 component GPS { /* tags power = 2500 mW] */ } calculations
6 component GPS gps1 /* tags power = 2 W */ ; }
language-implementation-specific OCL constraint would ref- evaluated OCL constraint witness is a valid C&C model,
and C&C model printed with all tags used in the aggregation
erence the type ConnectorSymbol in Fig. 3, l. 3 rather
than the general C&C type Con from Def. 1. Fig. 5: Positive witness that component gps1 satisfies OCL constraint from
Fig. 4: its power consumption is below the power consumption of its type
To address this problem, we decided to extend our OCL
implementation to support importing of configuration files. A
configuration file serves as a bridge from the mathematical V. D EFINING EFP C ONSTRAINTS IN OCL
definitions to the implementation-specific classes. Configura-
This section presents our second contribution: extending
tion files contain rewrite rules that rewrite names of C&C
OCL with support for measurement units in order to allow
elements from Def. 1 and Def. 2 to implementation-specific
modeling of EFP consistency constraints in OCL and to auto-
OCL expressions. This concept is generic and extensible
matically generate witnesses for OCL constraint consistency
to multiple target implementations. The C&C model OCL
or inconsistency. The OCL constraints follow the selection, ag-
constraints can be reused with different C&C meta-models
gregation, and comparison structure of EFP value consistency
as long all rewrite rules can be expressed using corresponding
rules (Def. 3) we introduced in [12].
meta-model-specific OCL expressions.
We structure this section by examples presenting different
The bottom part in Fig. 3 shows an excerpt of our Mon- features of our OCL framework. The examples we show are an
tiArc specific configuration file, which provides C&C spe- OCL constraint for InstPower (Rule 1) with a generated posi-
cific functions in OCL constraints. It imports all required, tive witness, an OCL constraint for CompPower (Rule 3) with
implementation-specific Java classes (Fig. 3, bottom, l. 5) a generated negative witness, and finally an OCL constraint
and contains rewrite rules (ll.7-10), similar to C prepro- for WCET Multi Core (Rule 6), which is the most complex
cessor’s #define macros, to map C&C domain names to example based on connection properties of C&C models.
implementation-specific names. In addition to rewrite rules, the
configuration file imports and provides graph functions (Fig. 3, A. Example: Power Consumption for Component Instantiation
bottom, l. 6) with C&C specific method implementations. For Fig. 4 shows the complete OCL code for instantiation
example, the function paths computes all C&C elements consistency of EFP power (Rule 1). Lines 1 and 2 import the
(components, ports, and connectors) on a path connecting configuration files for C&C specific extensions (see Sect. IV
an input to an output port. As another example, these graph above) as well as for EFP extensions containing special helper
functions can easily express the OCL invariant that each output functions (such as min, max, or sum) with units as parame-
port depends on at least one input port. ters. Including the configuration file EFPExt.conf ensures
The complete configuration file for rewriting C&C concepts that all OCL constraints follow the structure of Def. 3 with
into MontiArc concepts consists of 11 rewrite rules and a check (Fig. 4, l. 4), selection (selectedValue in Fig. 4,
imports 12 helper functions for use in C&C model specific l. 6), aggregation (aggregatedValue in Fig. 4, l. 7), and
constraints. There are two kinds of helper functions. The first a comparison (Fig. 4, ll. 9-10) element. Component instances
kind consists of graph-based functions that return a graph or without power tags are assigned the value 0W (Fig. 4, l. 7) and
chains of C&C elements connected (directly or indirectly) by component type definitions without power tags are assigned
two given C&C elements; they come in different versions to the value +ooW (Fig. 4, l. 10). These interpretations are up to
return only specific C&C elements (e.g., only components, or the engineers defining the consistency rule.
only components and ports), to avoid creating large graphs All components in our example C&C model in Fig. 1
with unnecessary elements and accelerate the verification satisfy the OCL constraint from Fig. 4. In case of satisfaction
process. The second kind of helper functions are mathematical our tool can generate a positive witness. Fig. 5 shows a
helper functions for EFPs such as min, max, sum, prod, (textual) positive witness that component gps1 satisfies the
union, or intersection. OCL constraint from Fig. 4: its power consumption is below
1 import CnCExt; OCL 1 import CnCExt; OCL
2 import EFPExt; 2 import EFPExt;
3 ocl ruleCompPower { 3 ocl ruleCompWCETInf {
4 context CTDef ct inv: // checks: ∈ 4 context Cmp cmp inv: // checks: ∈
5 let 5 let // selection: ≔ !" # ( )
6 selectedValues = ct.CSubs; // selection: ≔ . 8 selectedPaths = directSubCmpPaths(cmp);
7 // aggregation: ≔∑ , ∈ . // aggregation: ≔ {∑ . ∈
∈
8 aggregatedTags = List{max(s.CType.power, 0 W) | 7 aggregatedValues = List{sum(selVals, 0s) |
9 s in selectedValues}; 8 path in selectedPaths, selVals = List{
10 aggregatedValue = sum(aggregatedTags, 0 W); 9 max(elem.wcet, 0 s) | elem in path}};
in needed to have a value if aggregatedTags is empty 10 in
11
12 aggregatedValue <= 11 forall a in aggregatedValues:
// comparison: ≤ . // comparison: ∀ ∈ : ≤ .
13 min(ct.power,+ooW); } 12 (a < min(cmp.wcet, +oo s)) }
Fig. 6: OCL constraint for composition consistency of EFP power (Rule 3) Fig. 8: OCL constraint for composition consistency of EFP wcet (Rule 6)
WBalloonSens power=5W (aggregated value = 5.41 W)
C&C 2500mW + 2500mW + 10mW ) is greater than the power
wBalloonSens
tag value of component type definition WBalloonSens.
Temp power=400mW Controller power=10mW
temp controller
C. Example: Worst-Case Execution Time
Fig. 8 shows the complete OCL code for composition
GPS power=2500mW
gps2
only elements in selection of OCL consistency of EFP value wcet (Rule 6, multi core).
consistency rule are displayed The OCL variable selectedPaths in l. 6 stores a list
GPS power=2500mW of paths, which are lists of subcomponents. For each path in
gps1 the list, ll. 7-9 calculate the WCET value by summation of the
values on the path, and ll. 11-12 compare each value in the list
Fig. 7: Negative witness that component type WBalloonSens violates the against the WCET value of the parent component. Storing the
OCL constraint from Fig. 6: the combined power consumption of subcompo- list instead of the maximal value in the aggregatedValues
nents exceeds the parent’s power consumption
variable makes generated witnesses easier to understand: wit-
nesses will contain all paths instead of only one value.
The positive witness that component wBalloonSens sat-
the power consumption of its type GPS. Note that our OCL
isfies the OCL constraint of Fig. 8 contains the following
engine automatically uses the correct interpretation of the
selectedPaths with their aggregatedValues:
different units mW in tag of GPS and W in tag of gps1.
The witness is meant to help the engineer in understanding • wBalloonSens → controller → wBalloonSens with
the reasons for consistency. It contains the checked C&C 50ms ≤ 2s
• temp→controller→wBalloonSens with 550ms ≤ 2s
element, i.e., component instance gps1 (Fig. 5, l. 6), the
• gps1→controller→wBalloonSens with 1000ms ≤ 2s
selected elements to check against, i.e., component type GPS
• gps2→controller→wBalloonSens with 800ms ≤ 2s
(l. 5), and all EFP tags used for the computation of the
aggregated value (l. 3) and in the comparison step. VI. I MPLEMENTATION
Witness generation is completely automated for the satis- Our consistency verification tool takes a textual MontiArc
faction or violation of consistency rules. Our tool relies on the C&C model, EFP tag files tagging the C&C model, and an
structure of the OCL constraints following Def. 3 to construct OCL constraint as input. The verification process is fully
meaningful witnesses. Concretely, the witnesses contain the automated and consists of the following steps: (1) process the
checked element (context of OCL invariant), the elements textual model (parsing text to an AST and creating symbol
selected for comparison (OCL variable selectedValue(s), table) using the MontiCore framework [9]; (2) process the
or selectedPaths), all EFP tags appearing in the aggrega- textual OCL constraint; (3) execute all rewrite rules of all
tion (computation of OCL variable aggregatedValue(s)), imported configuration files; (4) generate Java code from the
and all EFP tags appearing in the final comparison. To further OCL constraint based on the AST and symbol table; and (5)
demonstrate satisfaction or violation, the aggregated value is execute the generated Java code to check the C&C model for
shown within the witness. consistency and to generate witnesses.
One challenge for implementing the generation of Java code
B. Example: Power Consumption for Component Definitions
from OCL was that while OCL is a type-less language, Java
Fig. 6 shows the complete OCL code for composition requires types for every declaration. Our generator infers the
consistency of EFP value power (Rule 3). variable types from OCL by looking up the return types of
Our running example does not satisfy the consistency rule invoked functions and propagating these types through nested
in Fig. 6, and a negative witness is generated for component List constructs (e.g., ll. 7-9 in Fig. 8).
type definition WBalloonSens. The graphical representation Another challenge was adding a unit concept to OCL.
of the generated negative witness in Fig. 7 shows the reason for Many EFPs contain values with measurement units. Thus
inconsistency: the aggregated value of 5.41 W (400mW + we developed an additional language SIUnit, which our
TABLE I: Verification time
C. Results:
C&C Model
Verification/
compilation
Generation
Table I shows running times in seconds for each EFP type
OCL2Java
Generator
Witness
Parsing
Parsing
checked (Rule 1 to Rule 6) and selected C&C model (small
Model
Total
OCL
Java
EFP
and complete). A close inspection of running times reveals
InstPower
small 1.6s 3.3s 0.2s 0.5s 0.1s 5.7s that each C&C model is loaded in 1.6-3.2s, depending on
complete 3.2s 3.3s 0.2s 0.5s 0.1s 7.3s its size; running time for parsing the short OCL constraints
small 1.6s 10.0s 0.2s 0.5s 3.5s 15.7s
CompPower is longer due to parser backtracking for nested mathematical
complete 3.2s 10.0s 0.2s 0.5s 6.8s 20.7s
WCET- small 1.6s 16.3s 0.2s 0.5s 19.0s 38.0s expressions and varies between 3-34s, transforming them into
Single Core complete 3.2s 16.3s 0.2s 0.5s 20.0s 39.0s
WCET- small 1.6s 34.0s 0.2s 0.5s 11.0s 47.0s executable code (this includes rewriting and type inference)
Multi Core complete 3.2s 34.0s 0.2s 0.5s 183.0s 221.0s needs less than 1s. Then, the actual execution of the veri-
fication code, i.e., checking the 119 or 1,396 components,
and witness generation, ranges from 0.1s for single-value
OCL implementation extends. SIUnit is capable of parsing aggregations to 183s for nested lists aggregations.
imperial, SI, and unofficial SI units [26] with metric prefixes This leads us to the following answers to our research ques-
and derived constructs, e.g., 28.2km/h and 9.81m·s−2 . It tions. (RQ1) We can automatically verify the consistency of
supports additional symbols for plus and minus infinity. For EFP values of an industrial sized model in reasonable running
unit conversions we use the JScience framework. times. (RQ2) It is interesting to see that OCL processing times
and running times for verification and witness generation are
VII. C ASE S TUDY ON ADAS consuming most of the time. However, the OCL processing
In our case study we want to evaluate the following two step for code generation has to be executed only once (and
research questions: every time a consistency rule changes). Finally, one may
RQ1 Does our framework scale to large industry provided separate verification from witness generation in order to speed
C&C models? up consistency checking when witnesses are not required.
RQ2 Which steps of automated EFP value consistency check- For inspection and further research we make all mentioned
ing are most time consuming? C&C models and OCL constraints used in our case study
available at:
A. Case Study Data: http://www.se-rwth.de/materials/OCLVerifyTool4CnCEFP.zip
For our case study we used a C&C model of an Au- VIII. R ELATED W ORK
tonomous Driver Assistance System (ADAS) provided by Acme [5] allows one to specify first-order predicates on the
Daimler AG. The available model did not contain EFP values. structure of architectures, dealing, e.g., with connectedness of
Therefore, we derived values for EFP wcet and power tags components. Our extension of OCL for C&C models provides
from reference materials and by evaluation as follows. To similar features. However, to the best of our knowledge the
approximate realistic EFP values for wcet, we have translated constraint language of Acme does not support EFPs.
the Simulink models to C-Code, compile this C-Code to Grunske [6] presents an evaluation framework for EFPs,
assembler code for a 16-bit Infineon C166 processor, and consisting of four elements. We focus on defining and check-
calculated WCETs based on the assembler instructions and ing consistency rules rather than on evaluation of EFPs.
the chip’s official documentation [23]. To approximate realistic Nevertheless, Grunske [6] also observed the need for a general
EFP values for power, we followed [15] to estimate power language to formulate evaluation of different EFP types.
consumption based on the assembly operations. The complete Sentilles et al. [21] present a meta-model for integrating
ADAS model contains 1,396 components, 4,438 ports, and non-functional properties into C&C models. They focus on
2,738 EFP values. handling multiple EFPs for the same entity and did not
implement rules for EFP consistency.
B. Execution: Cicchetti et al. [2] introduce a framework for evolution
We executed all tests on an ordinary computer with Win- of EFP values and present, as an example, how the change
dows 7 64-bit OS, an Intel Core i5-4590 CPU with four cores, of the WCET of a component requires updating the WCET
no hyperthreading and 3.3 GHz base frequency, and 8 GB of its parent component. To define validity conditions, they
RAM. First, we checked the consistency constraints defined use the Epsilon Validation Language [27], which is similar to
in Sect. V against a small, stripped down version of the OCL. It is possible to extend our framework to support similar
ADAS model, which consists of 119 components and 366 port evolution scenarios.
instances, enriched with 238 EFP values. Second, we checked Leveque and Sentilles [10] present refinement of EFPs
the consistency constraints against the complete ADAS through instantiation and subtyping of components. Engineers
model, which consists of 1,396 components and 4,438 port can use OCL constraints to filter EFP attributes of components.
instances, enriched with 2,738 EFP values. These model sizes The OCL constraints are written against the meta-model of the
and numbers of EFP values show the necessity for automatic C&C implementation. We use C&C-specific OCL constraints
consistency checks. to define consistency rules beyond component EFP refinement.
Finally, Sapienza et al. [20] present EFP consistency rules [7] A. Haber, J. O. Ringert, and B. Rumpe. MontiArc - Architectural Mod-
for component composition. The tools used in [20] and a eling of Interactive Distributed and Cyber-Physical Systems. Technical
Report AIB-2012-03, RWTH Aachen, february 2012.
related case study [22] go beyond information stored with [8] F. Huber, B. Schätz, A. Schmidt, and K. Spies. Autofocus: A tool for
model elements, e.g., they measure EFP values by simulation. distributed systems specification. In FTRTFT, 1996.
It is unclear whether their approach can be easily extended to [9] H. Krahn, B. Rumpe, and S. Völkel. Monticore: a framework for
additional or alternative EFP constraints. compositional development of domain specific languages. In STTT,
volume 12, 2010.
IX. C ONCLUSION [10] T. Leveque and S. Sentilles. Refining extra-functional property values
in hierarchical component models. In CBSE, 2011.
We presented an OCL framework and tool for the descrip- [11] S. Maoz, J. O. Ringert, and B. Rumpe. Synthesis of component and
tion and verification of consistency rules of EFPs in C&C connector models from crosscutting structural views. In FSE, 2013.
[12] S. Maoz, J. O. Ringert, B. Rumpe, and M. von Wenckstern. Consistent
models. The work includes a C&C-specific extension of OCL extra-functional properties tagging for component and connector models.
with native support for measurement units, and an automatic In ModComp, 2016.
mechanism for verifying consistency and producing witnesses [13] N. Medvidovic and R. Taylor. A Classification and Comparison
for EFP consistency checking results. We implemented the ap- Framework for Software Architecture Description Languages. IEEE
Transactions on Software Engineering, 2000.
proach within the MontiCore framework for the C&C model- [14] P. Mir Seyed Nazari. MontiCore: Efficient Development of Composed
ing language MontiArc. Our initial evaluation on an industrial Modeling Language Essentials. Shaker, 2017.
sized model shows that it is expressive and scales to large C&C [15] S. Nikolaidis, N. Kavvadias, P. Neofotistos, K. Kosmatopoulos,
T. Laopoulos, and L. Bisdounis. Instrumentation set-up for instruction
models. Our framework works for comparable extra-functional level power modeling. In PATMOS, 2002.
properties, these include quantitative properties (e.g., worst- [16] A. Rawashdeh and B. Matalkah. A new software quality model for
case execution time, power, or memory consumption) and evaluating COTS components. Journal of Computer Science, 2(4), 2006.
qualitative properties (e.g., traceability, portability flags, ASIL [17] J. O. Ringert. Analysis and Synthesis of Interactive Component and
Connector Systems. Aachener Informatik-Berichte, Software Engineer-
security, or encryption levels). ing, Band 19. Shaker Verlag, 2014.
[18] G. C. Roman. A taxonomy of current issues in requirements engineering.
Acknowledgements This research was supported by a Grant Computer, 18(4), April 1985.
from the GIF, the German-Israeli Foundation for Scientific [19] M. Saadatmand, A. Cicchetti, and M. Sjödin. UML-based modeling of
Research and Development. non-functional requirements in telecommunication systems. In ICSEA,
2011.
R EFERENCES [20] G. Sapienza, S. Sentilles, I. Crnkovic, and T. Seceleanu. Extra-functional
properties composability for embedded systems partitioning. In CBSE,
[1] J. P. Cavano and J. A. McCall. A framework for the measurement of 2016.
software quality. SIGSOFT Softw. Eng. Notes, 3(5), 1978.
[21] S. Sentilles, P. Stepan, J. Carlson, and I. Crnkovic. Integration of extra-
[2] A. Cicchetti, F. Ciccozzi, T. Leveque, and S. Sentilles. Evolution man-
functional properties in component models. In CBSE, 2009.
agement of extra-functional properties in component-based embedded
systems. In CBSE, 2011. [22] J. Suryadevara, G. Sapienza, C. C. Seceleanu, T. Seceleanu, S. E.
[3] P. H. Feiler and D. P. Gluch. Model-Based Engineering with AADL: Ellevseth, and P. Pettersson. Wind turbine system: An industrial case
An Introduction to the SAE Architecture Analysis & Design Language. study in formal modeling and verification. In FTSCS, 2013.
Addison-Wesley, 2012. [23] Infineon website. https://www.infineon.com. Retrieved 10/07/17.
[4] D. Garlan, R. T. Monroe, and D. Wile. Acme: An architecture [24] MathWorks Simulink. http://www.mathworks.com/products/simulink/.
description interchange language. In CASCON, 1997. [25] OMG Object Constraint Language 2.4. http://www.omg.org/spec/OCL/
[5] D. Garlan, R. T. Monroe, and D. Wile. Acme: Architectural description 2.4/. Retrieved 10/07/17.
of component-based systems. In Foundations of Component-Based [26] SI Units – Wikipedia. https://en.wikipedia.org/wiki/International_
Systems. Cambridge University Press, 2000. System_of_Units. Retrieved 10/07/17.
[6] L. Grunske. Early quality prediction of component-based systems - A [27] The Epsilon Book. http://www.eclipse.org/epsilon/doc/book/. Retrieved
generic framework. Journal of Systems and Software, 80(5), 2007. 10/07/17.