-We present an OCL framework and tool for the description and verification of consistency rules of extra-functional properties (EFPs) in component and connector (C&C) models. The framework is based on our previously defined structure of EFP consistency rules using selection, aggregation, and comparison operators, and provides C&C specific OCL functions and configurations that allow engineers to succinctly express EFP consistency rules for C&C models. Further, the extension of OCL is twofold. First, constraints may contain C&C specific expressions and second, expressions natively support measurement units as required in specifications of EFPs. We have extended the OCL verification process to support the novel extensions and to automatically generate meaningful positive and negative witnesses for consistency and inconsistency. We implemented the approach within the MontiCore framework for the C&C modeling language MontiArc. Initial evaluation shows that it is expressive and scales to large, industrial sized C&C models.
Component and connector (C&C) models are used in many
application domains of software engineering, from
cyberphysical and embedded systems to web services and enterprise
applications. The structure of C&C models consists of
components at different containment levels, their typed interaction
points, and connectors between them [
Recently, we have presented a non-invasive technique for
adding EFPs to C&C models by means of tagging
languages [
In this paper we are interested in the concrete formalization
of EFP consistency rules and in their automated analysis.
We propose to leverage the popular and expressive Object
Constraint Language [
Our first contribution is a C&C-specific extension of OCL. The extension allows the definition of C&C consistency constraints based on clean mathematical C&C definitions; all implementation specific details, such as more complex types from the meta-model or abstract-syntax representations are abstracted away by providing C&C specific OCL configurations and powerful type-inference mechanisms when checking consistency.
Our second contribution extends OCL with support
for measurement units and an automatic mechanism to
produce witnesses for EFP consistency checking results.
First, many EFPs, describing physical properties of C&C
models, e.g., WCET, power consumption, or memory usage,
contain physical units, e.g., seconds, Watts, or sizes. Thus,
to enable domain experts define EFP consistency rules, a
constraint language for EFPs naturally should support
automatic unit comparison and conversion . Second, our previously
defined mathematical framework [
Our third contribution is an initial evaluation of checking EFP consistency of an industrial sized C&C model. Specifically, we used our tool to verify four selected consistency rules on an industrial sized Autonomous Driver Assistance System (ADAS) model. The ADAS model consists of about 1,400 components and 4,500 ports, and 2,800 tagged EFP values. Our examples and evaluation show that (i) our OCL based approached is expressive enough for defining complex consistency constraints, and (ii) that the performance of our implementation for checking these consistency rules scales to large models.
In the next section we present a running example. Sect. III gives background on C&C models and consistency rules of EFPs. Sect. IV and Sect. V present our OCL framework and example constraints, Sect. VI presents the implementation, and Sect. VII presents a case study in which the framework is used. Sect. VIII present related work, and Sect. IX concludes.
component type instance name block of component type WBalloonSens consists of various components: a temperature sensor (component instance temp of component type Temp), two GPS sensors (component instances gps1 and gps2 of component type GPS), and a controller (component instance controller of component type Controller). The controller periodically pushes sensor data to another system in order to save it. The position of the balloon is important for recovery after landing. Position data from GPS is pushed to an antenna system, which relays the position to ground control.
One EFP in our running example is power consumption (tag power). The component types and the component instances in Fig. 1 are tagged with estimated power consumption, e.g., the component type GPS is tagged with power=2500mW and its component instance gps1 is tagged with power=2W. The weather balloon will be running on a limited power supply and power consumption has to be budgeted carefully. Hence, the sensor block is required to consume at most 5W (see power property of component type WBalloonSens in Fig. 1). Based on this extra-functional property of the parent component requirements for subcomponent types are added: Temp consumes at most 400mW , the GPS sensors GPS 2500mW each, and the controller 10mW .
However, the declaration of power consumption EFPs in this model is inconsistent. The subcomponents require 5410mW when only 5W are defined by component type WBalloonSens (note that it would be consistent when taking the component instances and not types into account, which together consume 4910mW ).
Another EFP in our running example is the worst-caseexecution-time (WCET, tag wcet) of components. As we assume independent execution of all components and the WCET of each subcomponent is less than the WCET of component type WBalloonSens, the WCET EFPs are consistent.
Engineers can easily add EFP tags and EFP consistency rules as OCL constraints, which our tool automatically verifies. 1component WBalloonSens { 2 ports in Byte[] controlSig, 3 out Byte[] dataSave, 4 out Byte[] dataAntenna; 5 component Controller controller; 6 component GPS gps1, gps2; 7 component Temperature temp; 8 ... 9 connect controller.antenna -> dataAntenna; 10 connect gps1.loc -> controller.loc1; } e v a S a tad Fig. 2: Definitions of WBalloonSens from Fig. 1 top component definition is instantiated once with instance name wBalloonSens
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 [
C&C model is a structure cncm = hCmps; Ports; Cons; Types; subs; ports; typei where
Cmps is a set of named components, cmp 2 Cmps has a set of ports ports(cmp) Ports and a (possibly empty) set of immediate subcomponents subs(cmp) Cmps, Ports = InPorts ] OutPorts is a disjoint union of input and output ports where each port p 2 Ports has a name, a type type(p) 2 Types, and belongs to exactly one component p 2 ports(cmp), Cons is a set of directed connectors con 2 Cons, each of which connects two ports con:src; con:tgt 2 Ports of the same type, which belong to two sibling components or to a parent component and one of its immediate subcomponents, and
Types is a finite set of type names.
C&C models from Def. 1 are well-formed iff no component
is its own (transitive) subcomponent and has at most one direct
parent and subcomponents are connected legally (see [
While some formalisms directly express C&C models, e.g.,
[
ponent type definition is a structure ct = hcType; CPorts; CSubs; CConsi 2 CTDefs where cType uniquely identifies the component type, CPorts is a set of input and output port definitions where each port p 2 CPorts has a name and a type, CSubs N ame CTDefs is a set of named subcomponent declarations, and CCons is a set of directed connector definitions con 2 CCons, each of which connects two port definitions con:src; con:tgt of the same type, which belong to two sibling subcomponent declarations or to a component type definition and one of its subcomponent declarations.
A component type t 2 CTDefs is instantiated to a C&C
model by creating a component for c with subcomponents,
that are instances of t:CSubs with connectors according
to t:CCons. For a more detailed definition including
wellformedness rules and instantiation see [
It is important to note that the consistency of an EFP value may depend on multiple other C&C model elements, their relations, and their EFP values. Some advanced examples of consistency relate to component instantiation and composition in C&C models. In addition, consistency may be very specific to the EFP type, e.g., checking consistency of WCET values is different from checking memory consumption.
To address the challenge of ensuring consistency of EFP
values, in a previous paper [
tency rule is a structure consisting of: checks name of tag and element checked by rule; selection selects relevant C&C elements to check consistency; aggregation aggregates values of selected elements; and comparison compares values to decide consistency.
The next two subsections illustrate some examples on
consistency definition rules according to Def. 3; more examples
are available in [
1) Instantiation Consistency: Instantiation consistency checks whether the EFPs of component instances are consistent to the EFPs of their component type definitions.
Rule 1 (InstPower [
Rule 2 (InstCertificates): The certificates of component instances must be at most the certificates common to all ports of the component: checks: tag cert of cmp 2 Cmps selection: P := cmp:ports aggregation: v := Tp2P p:cert comparison: v cmp:cert 2) Composition Consistency: Composition consistency checks whether the EFPs of C&C model elements are consistent across their composition. The following example rules address consistency at the type level. Similar rules can be defined at the instance level.
Rule 3 (CompPower [
(name;sct)2S comparison: v ct:power
Rule 4 (ASIL): The ASIL (Automotive Safety Integrity Level) of all subcomponents must be higher or equal than the ASIL of the composed component: checks: tag asil of cmp 2 Cmps selection: S := cmp:subs aggregation: v := min number(sc:asil)1
sc2S comparison: v number(cmp:asil)
Rule 5 (WCET Single Core): The WCET of a component instance is at most the WCET of its subcomponent instances. checks: tag wcet of cmp 2 Cmps selection: S := cmp:subs aggregation: v := P sc:wcet
csmc2pS:wcet comparison: v
Rule 6 (WCET Multi Core): The WCET of a component instance is at most the maximum of the WCET of parallel executable direct subcomponent paths.
checks: tag wcet of cmp 2 Cmps selection: S := directSubCmpP aths(cmp) 2 aggregation: v := max P elem:wcet
path2S elem2path comparison: v cmp:wcet
Note that our framework does not limit the selection,
aggregation, and comparison operators in any way. Our previous
paper [
This section presents our first contribution: a C&C-specific extension of OCL.
We start with an example. The top part in Fig. 3 presents
an OCL invariant expressing that the source and target
ports of a connector have the same data type (l. 3).
Typically, OCL constraints are written against a concrete
metamodel; this, however, makes the OCL constraints
dependent on a specific language implementation. As an
example, our C&C language implementation MontiArc
provides references to all connectors in a C&C model by:
List<ConnectorSymbol> connectors =
globalScope.resolve(ConnectorSymbol.KIND) [
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 definitions to the implementation-specific classes. Configuration files contain rewrite rules that rewrite names of C&C elements from Def. 1 and Def. 2 to implementation-specific OCL expressions. This concept is generic and extensible to multiple target implementations. The C&C model OCL constraints can be reused with different C&C meta-models as long all rewrite rules can be expressed using corresponding meta-model-specific OCL expressions.
The bottom part in Fig. 3 shows an excerpt of our MontiArc specific configuration file, which provides C&C specific functions in OCL constraints. It imports all required, implementation-specific Java classes (Fig. 3, bottom, l. 5) and contains rewrite rules (ll.7-10), similar to C preprocessor’s #define macros, to map C&C domain names to implementation-specific names. In addition to rewrite rules, the configuration file imports and provides graph functions (Fig. 3, bottom, l. 6) with C&C specific method implementations. For example, the function paths computes all C&C elements (components, ports, and connectors) on a path connecting an input to an output port. As another example, these graph functions can easily express the OCL invariant that each output port depends on at least one input port.
The complete configuration file for rewriting C&C concepts into MontiArc concepts consists of 11 rewrite rules and imports 12 helper functions for use in C&C model specific constraints. There are two kinds of helper functions. The first kind consists of graph-based functions that return a graph or chains of C&C elements connected (directly or indirectly) by two given C&C elements; they come in different versions to return only specific C&C elements (e.g., only components, or only components and ports), to avoid creating large graphs with unnecessary elements and accelerate the verification process. The second kind of helper functions are mathematical helper functions for EFPs such as min, max, sum, prod, union, or intersection. 1import CnCExt; 2import EFPExt; 3ocl ruleInstPower { 4 context Cmp cmp inv: // checks: ∈ 5 let 6 selectedValue = cmp.CType; // selection: ≔ ( ) ∈ 7 aggregatedValue = max(cmp.power, 0W);// aggregation: ≔ . 8 in consider maximum value of the power tags, and “0W” if power tag is missing 109 agmgirne(gsaetleedcVtaelduVeal<u=e.power,+ooW); } // comparison: ≤ . Fig. 4: OCL constraint for instantiation consistency of EFP power (Rule 1) 1// positive witness for checking: shows if positive or negative witness 2// ocl "ruleInstPower.ocl" on model "WBalloonSens.ma" 34/c/omapgognreengtatWeBdalvlaolouneSeinns m{odel: 2 W aggregateducsoveamfluuplelefsox,r 5 component GPS { /* tags power = 2500 mW] */ } calculations 6 component GPS gps1 /* tags power = 2 W */ ; } eavnadluCa&teCdmOoCdLelconstraint pwriitnnteesdswisitha avlalltidagCs&uCsemdoindethl,e aggregation
This section presents our second contribution: extending
OCL with support for measurement units in order to allow
modeling of EFP consistency constraints in OCL and to
automatically generate witnesses for OCL constraint consistency
or inconsistency. The OCL constraints follow the selection,
aggregation, and comparison structure of EFP value consistency
rules (Def. 3) we introduced in [
We structure this section by examples presenting different features of our OCL framework. The examples we show are an OCL constraint for InstPower (Rule 1) with a generated positive witness, an OCL constraint for CompPower (Rule 3) with a generated negative witness, and finally an OCL constraint for WCET Multi Core (Rule 6), which is the most complex example based on connection properties of C&C models.
Fig. 4 shows the complete OCL code for instantiation consistency of EFP power (Rule 1). Lines 1 and 2 import the configuration files for C&C specific extensions (see Sect. IV above) as well as for EFP extensions containing special helper functions (such as min, max, or sum) with units as parameters. Including the configuration file EFPExt.conf ensures that all OCL constraints follow the structure of Def. 3 with a check (Fig. 4, l. 4), selection (selectedValue in Fig. 4, l. 6), aggregation (aggregatedValue in Fig. 4, l. 7), and a comparison (Fig. 4, ll. 9-10) element. Component instances without power tags are assigned the value 0W (Fig. 4, l. 7) and component type definitions without power tags are assigned the value +ooW (Fig. 4, l. 10). These interpretations are up to the engineers defining the consistency rule.
All components in our example C&C model in Fig. 1 satisfy the OCL constraint from Fig. 4. In case of satisfaction our tool can generate a positive witness. Fig. 5 shows a (textual) positive witness that component gps1 satisfies the OCL constraint from Fig. 4: its power consumption is below the power consumption of its type GPS. Note that our OCL engine automatically uses the correct interpretation of the different units mW in tag of GPS and W in tag of gps1.
The witness is meant to help the engineer in understanding the reasons for consistency. It contains the checked C&C element, i.e., component instance gps1 (Fig. 5, l. 6), the selected elements to check against, i.e., component type GPS (l. 5), and all EFP tags used for the computation of the aggregated value (l. 3) and in the comparison step.
Witness generation is completely automated for the satisfaction or violation of consistency rules. Our tool relies on the structure of the OCL constraints following Def. 3 to construct meaningful witnesses. Concretely, the witnesses contain the checked element (context of OCL invariant), the elements selected for comparison (OCL variable selectedValue(s), or selectedPaths), all EFP tags appearing in the aggregation (computation of OCL variable aggregatedValue(s)), and all EFP tags appearing in the final comparison. To further demonstrate satisfaction or violation, the aggregated value is shown within the witness.
Fig. 6 shows the complete OCL code for composition consistency of EFP value power (Rule 3).
Our running example does not satisfy the consistency rule in Fig. 6, and a negative witness is generated for component type definition WBalloonSens. The graphical representation of the generated negative witness in Fig. 7 shows the reason for inconsistency: the aggregated value of 5.41 W (400mW + 2500mW + 2500mW + 10mW ) is greater than the power tag value of component type definition WBalloonSens.
Fig. 8 shows the complete OCL code for composition consistency of EFP value wcet (Rule 6, multi core).
The OCL variable selectedPaths in l. 6 stores a list of paths, which are lists of subcomponents. For each path in 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 against the WCET value of the parent component. Storing the list instead of the maximal value in the aggregatedValues variable makes generated witnesses easier to understand: witnesses will contain all paths instead of only one value.
The positive witness that component wBalloonSens satisfies the OCL constraint of Fig. 8 contains the following selectedPaths with their aggregatedValues: wBalloonSens ! controller ! wBalloonSens with 50ms 2s temp!controller!wBalloonSens with 550ms 2s gps1!controller!wBalloonSens with 1000ms 2s gps2!controller!wBalloonSens with 800ms 2s
Our consistency verification tool takes a textual MontiArc
C&C model, EFP tag files tagging the C&C model, and an
OCL constraint as input. The verification process is fully
automated and consists of the following steps: (1) process the
textual model (parsing text to an AST and creating symbol
table) using the MontiCore framework [
One challenge for implementing the generation of Java code from OCL was that while OCL is a type-less language, Java requires types for every declaration. Our generator infers the variable types from OCL by looking up the return types of invoked functions and propagating these types through nested List constructs (e.g., ll. 7-9 in Fig. 8).
Another challenge was adding a unit concept to OCL.
Many EFPs contain values with measurement units. Thus
we developed an additional language SIUnit, which our
OCL implementation extends. SIUnit is capable of parsing
imperial, SI, and unofficial SI units [
RQ1 Does our framework scale to large industry provided
C&C models? RQ2 Which steps of automated EFP value consistency checking are most time consuming?
For our case study we used a C&C model of an
Autonomous Driver Assistance System (ADAS) provided by
Daimler AG. The available model did not contain EFP values.
Therefore, we derived values for EFP wcet and power tags
from reference materials and by evaluation as follows. To
approximate realistic EFP values for wcet, we have translated
the Simulink models to C-Code, compile this C-Code to
assembler code for a 16-bit Infineon C166 processor, and
calculated WCETs based on the assembler instructions and
the chip’s official documentation [
We executed all tests on an ordinary computer with Windows 7 64-bit OS, an Intel Core i5-4590 CPU with four cores, no hyperthreading and 3.3 GHz base frequency, and 8 GB RAM. First, we checked the consistency constraints defined in Sect. V against a small, stripped down version of the ADAS model, which consists of 119 components and 366 port instances, enriched with 238 EFP values. Second, we checked the consistency constraints against the complete ADAS model, which consists of 1,396 components and 4,438 port instances, enriched with 2,738 EFP values. These model sizes and numbers of EFP values show the necessity for automatic consistency checks.
Table I shows running times in seconds for each EFP type checked (Rule 1 to Rule 6) and selected C&C model (small and complete). A close inspection of running times reveals that each C&C model is loaded in 1.6-3.2s, depending on its size; running time for parsing the short OCL constraints is longer due to parser backtracking for nested mathematical expressions and varies between 3-34s, transforming them into executable code (this includes rewriting and type inference) needs less than 1s. Then, the actual execution of the verification code, i.e., checking the 119 or 1,396 components, and witness generation, ranges from 0.1s for single-value aggregations to 183s for nested lists aggregations.
This leads us to the following answers to our research questions. (RQ1) We can automatically verify the consistency of EFP values of an industrial sized model in reasonable running times. (RQ2) It is interesting to see that OCL processing times and running times for verification and witness generation are consuming most of the time. However, the OCL processing step for code generation has to be executed only once (and every time a consistency rule changes). Finally, one may separate verification from witness generation in order to speed up consistency checking when witnesses are not required.
For inspection and further research we make all mentioned C&C models and OCL constraints used in our case study available at: http://www.se-rwth.de/materials/OCLVerifyTool4CnCEFP.zip
Acme [
Grunske [
Sentilles et al. [
Cicchetti et al. [
Leveque and Sentilles [
Finally, Sapienza et al. [
We presented an OCL framework and tool for the description and verification of consistency rules of EFPs in C&C models. The work includes a C&C-specific extension of OCL with native support for measurement units, and an automatic mechanism for verifying consistency and producing witnesses for EFP consistency checking results. We implemented the approach within the MontiCore framework for the C&C modeling language MontiArc. Our initial evaluation on an industrial sized model shows that it is expressive and scales to large C&C models. Our framework works for comparable extra-functional properties, these include quantitative properties (e.g., worstcase execution time, power, or memory consumption) and qualitative properties (e.g., traceability, portability flags, ASIL security, or encryption levels).
Acknowledgements This research was supported by a Grant from the GIF, the German-Israeli Foundation for Scientific Research and Development.