Structural Contracts – Motivating Contracts to Ensure Extra-Functional Semantics

Abstract

In our work we aim at a composable and consistent specification and verification of contracts for extra-functional properties, such as power consumption or temperature. To this end, a necessary precondition for the semantical correctness of such properties is to ensure the structurally correct modeling of their interdependences.

While this can be solved by a tailoring of the Component Based Design (CmpBD) frameworks, the resulting design constraints are specific to tools and viewpoints, not being sufficiently configurable for the designers. To solve this problem within the contract framework, Contract Based Design (CBD) with explicit port variables provides also no configurable but sound methodology for structurally relating the properties between different components and views. For that, we propose the idea of structural contracts. Using implicit structural ports, structural guarantees can be given according to the Component Based Design structure. Expressing structural design constraints by the means of structural assumptions, the CmpBD constraints can become part of the Contract Based Design framework and, thus, can be checked for compatibility and refinement.

As a result, structural contracts enable the contract based specification and verification of structural rules for the correct modeling of functional and extra-functional interdependences. Providing both, property specifications and Component Based Design constraints by contracts, the approach is flexible and sound.

This work is supported by the ANCONA Project, funded by the German Federal Ministry of Research and Education (BMBF) under Grant Agreement 16ES021.

1 Introduction

Following the increasing opportunities to integrate more functionality and improved performance in today’s integrated microelectronic systems has lead to continuously growing design complexity and an increasing number and heterogeneity of design requirements. As a result, the specification, modeling and verification of such heterogeneous systems became a challenging task, requiring a reliable collaboration of specialists from different design and verification domains.

Following the paradigms of encapsulation, divide and conquer and separation of concerns the concepts of components and viewpoints have been introduced to master design complexity by Component Based Design (CmpBD) [9]. Commonly a component is considered to be a design element, which internally encapsulates its behavior, solely restricting its interaction with the environment to its well-defined port interface. Hence, a main precondition of Component Based Design is the components’ behaviors to be compositional. That means, that for each point of time the interaction between connected components is clearly determined by solely one of the components, controlling the information exchange across this connection without being affected by undelayed influence from the environment.

Additionally, considering the further refinement and implementation of subcomponents to proceed independently, the compatibility of connected ports has to be ensured. To this end, type systems [6] are applied, to declare the type of the components’ ports and to verify that connected ports have compatible types. Beyond the most common notion of untimed static types, such as boolean, integer etc., Contract Based Design (CBD) [3, 11] enables a more dynamic notion of compatibility. By the means of the contracts’ assumptions A all acceptable inputs of the components M are formally described by timed traces, declaring interconnections incompatible if the corresponding environment E is allowed to provide a timed sequence of outputs which violates the components’ assumptions. Differently, when the assumptions are satisfied, the components provide outputs according to the guarantee G, which correspond to the satisfied assumption.

Nevertheless, static type and compatibility checking of contracts is not flexible enough to be applicable for the consistent specification and verification of the interactions between the properties from multiple extra-functional viewpoints, largely comprising physical properties w. r. t. power or temperature etc. Differently, a more flexible declaration of designer-defined types would be necessary, to allow for complex, derived and configurable types, which appropriately combine the value and time semantics of the ports with a viewpoint-specific physical interpretation, such as ‘average power consumption per operation in ${\mu }W$’.

Considering viewpoint-specific models of a heterogeneous (multi-viewpoint) component to be viewpoint-specific components themselves, we assume that a sufficiently flexible but sound declaration and verification of designer-defined types can be achieved by extending the compatibility criteria of contracts to also structural properties, which constrain the basic design elements of the decomposition, such as the identifiers of components and ports. Since Contract Based Design allows contracts to constrain only the explicitly declared ports of components we propose a first concept of structural contracts. Based on an introspection of the component structure we implicitly instantiate a decomposition component plus structural ports and structural nets, to enable the contract based reflection of the component structure via these explicit ports. As a result, the usage of structural assumptions allows us to systematically constrain the instantiation and connection of subcomponents based on their component and port names.

To motivate our idea of structural contracts, Sect. 2 explains an artificial example, for which the extra-functional failure of the design becomes hidden – i.e. erroneously not visible – because of a semantically incorrect connection of extra-functional ports. Next, in Sect. 3 we summarize the related work, before we introduce the formal basics of components and contracts in Sect. 4. In Sect. 5 we present our approach of structural contracts based on the introspection, component extension and contract based reflection of the component structure. Then, in Sect. 6 we outline a first proof of concept, using our initial example to successfully invalidate the previously hidden false negative verification using structural contracts. In Sect. 7 we conclude and give an outlook to future work.

2 Motivating Example

To motivate structural contracts we consider the simplified, artificial example of a composed component M given in Fig. 1, which is specified to hold an average power consumption of at maximum $20 \mu \text {W}$. The component has one functional input port $\textit{x}_0$, indicating two different operating modes, and one extra-functional output port $\textit{y}_\textit{p}$, denoting the average power consumption per clock cycle.

Fig. 1.

Motivating example, composing a component M from subcomponents $M_i$, connecting their inputs $x_{(\cdot )}$ resp. outputs $y_{(\cdot )}$ from multiple extra-functional viewpoints (functional, capacitive load and power) by interconnecting nets $n_{(\cdot )}$ to evaluate the composed system’s power consumption.

Refining M by a composition of three different subcomponents, the subcomponents are $M_0$, $M_1$ and $M_2$, with all of them having one functional input $\textit{x}_0$ and one functional output $\textit{y}_0$, decoding their operating mode in one bit. Moreover, for the purpose of calculating the power consumption, the subcomponents provide inputs $\textit{x}_\textit{c}$ and outputs $\textit{y}_\textit{c}$, which describe the components’ input or load capacitance $\overline{\textit{C}}_\textit{sw}^{e}$, responsible for consuming a certain amount of power during the interaction of both components. Of course, in addition to that, each component consumes also an internal amount of power, based on the internally switched capacitance $\overline{\textit{C}}_\textit{sw}^{i}$. For simplification, the example contains no further ports for the supply voltage $V_\textit{DD}$ or clock frequency $f_\textit{clk}$, considering both of them to be constant at $V_\textit{DD} = 1.0 \text {V}$ and $f_\textit{clk} = 2.0\,\text {MHz}$ for components $\textit{M}_1$ and $\textit{M}_2$ and $\textit{M}_0.V_\textit{DD} = 1.0 \text {V}$ and $\textit{M}_0.f_\textit{clk} = 6.0\,\text {MHz}$ for component $\textit{M}_0$. Above that, following $\overline{\textit{P}} = \frac{1}{2} V_\textit{DD}^2 f_\textit{clk} \overline{\textit{C}}_\textit{sw}$ the average power consumption $\textit{y}_\textit{p} = \overline{\textit{P}}$ depends on the average switched capacitance $\overline{\textit{C}}_\textit{sw} = \overline{\textit{C}}_\textit{sw}^{i} + \overline{\textit{C}}_\textit{sw}^{e}$, internally resp. externally switched according to the functional activity of the component. Appropriately to these specifications, Table 1 outlines the functional and extra-functional behavior of the components w. r. t. their input resp. output ports. For example, the switched capacitance of $\textit{M}_\textit{1}$ is $3\text {pF}$ for $\textit{M}.\textit{x}_0 = 1$. This is because of $\overline{\textit{C}}_\textit{sw}^{i} = 2$ and $\textit{M}_1.\textit{x}_\textit{c} = \textit{M}_2.\textit{y}_c = \overline{\textit{C}}_\textit{sw}^{e} = 1$, following from exchanging the functional and extra-functional information according to the interconnection of Fig. 1, so that $\textit{M}_0.\textit{x}_0 = 1$, $\textit{M}_1.\textit{x}_0 = 1$ and $\textit{M}_2.\textit{x}_0 = 0$. As a result of this evaluation, the given composition of M finally does not hold the specification of an average power consumption of at maximum $20 \mu \text {W}$, consuming $23 \mu \text {W}$ for the case of $\textit{M}.\textit{x}_0 = 1$.

Table 1. Overview of the example’s functional and extra-functional component characteristics, which belong to the functional, capacitive load and power viewpoints. To consider the dependency on the functional inputs the expression $(\textit{x}_\textit{0} \,?\, a : b)$ shall logically denote $(\textit{x}_\textit{0} \rightarrow a) \wedge (\lnot \textit{x}_\textit{0} \rightarrow b)$.

Contrary to this, the same calculation of the power consumption asserts ‘valid’ when during refinement the following – semantically inconsistent – connection error occurs as given in Fig. 2. Refining M with $\textit{n}_6$ and $\textit{n}_7$ instead of $\textit{n}_1$ and $\textit{n}_3$, the externally switched capacitances $\textit{M}_0.\textit{y}_\textit{0}$ and $\textit{M}_1.\textit{y}_\textit{0}$ are interchanged, leading to the erroneous power calculation $\textit{M}.\textit{y}_\textit{0} = (\textit{x}_\textit{0} \,?\, 20 : 11)$ in Table 2.

Fig. 2.

Erroneous composition resp. refinement of M from the same subcomponents $M_i$, introducing semantically false connections $\textit{n}_6$ and $\textit{n}_7$ instead of $\textit{n}_1$ and $\textit{n}_3$, which violate the physical semantics of allocating the capacitive loads in correspondence with the real worlds functional interconnections $\textit{n}_0$ and $\textit{n}_2$, falsely verifying $\textit{M}.\overline{\textit{P}}<20\mu \text {W}$.

Table 2. Extra-functional characteristics of the erroneously refined example, leading to a false negative verification of the power consumption, satisfying $\textit{M}.\overline{\textit{P}}<20\mu \text {W}$.

Erroneously refining M with $\textit{n}_6$ and $\textit{n}_7$ instead of $\textit{n}_1$ and $\textit{n}_3$, the semantical meaning of the capacitive loads, corresponding to the real worlds functional interconnections $\textit{n}_0$ and $\textit{n}_2$ gets violated. Without the possibility of strictly relating these ports by some concepts of derived complex types, such – and similar – semantic errors can easily remain unrevealed. As a solution to this, we propose structural contracts, to allow the designers to add composition constraints, and an introspection and reflection of the component structure, making the structural decomposition part of the contract-based specification and verification approach.

3 Related Work

Considering the related work – to the authors’ best knowledge – no other work aims at ensuring the semantical consistency of different components and viewpoints – i.e. a verifiable but flexible type system with complex, designer-defined types – by a contract based formulation of constraints for the logical decomposition structure.

The probably most common approach to support semantical consistency and compatibility would be to provide only a limited set of fixed types of components and ports resp. design rules, which are defined and checked by the component based design framework. While this tailoring may support complex type systems, as e. g. the polymorphic and structured types [12] in Ptolemy II, it lacks flexibility w. r. t. defining viewpoint-specific compatibility and refinement rules, meaning constraints on how these types can bottom-up be constructed resp. top-down refined, checking value-, causality- and time-aware construction rules.

In interface theories [1, 2] the distinction between bottom-up components for compositional abstraction on the one hand, and top-down interfaces for compositional design on the other hand have lead to the general concepts of compatibility and refinement checking for component specifications using assumptions and guarantees. Applying timed languages to describe assumptions and guarantees, the contracts allow to specify and to verify the compatibility of the components’ interaction protocols according to value and time resp. causality criteria. Nevertheless – while building the general foundation for contracts based design – without some introspection and reflection of the interface variables and their interconnection relations via additional ports, top-down constraints w. r. t. the logical decomposition structure are not possible that way.

Differently, to investigate and define behavioral types, in [4, 5] the concepts of glue operators and glue constraints are defined for the BIP (behavior, interaction, priority) framework. Providing connectors with priorities and their own memoryless behavior the interaction between components connected by a connector can appropriately be synchronized w. r. t. to some timed or untimed causality relation. Hence, again compatibility is meant only in the sense of interaction protocols, not concerning extra-functional semantics of e. g. different viewpoints.

4 Formal Basics

As given in Fig. 1, Component Based Design allows to structurally compose the behavior of higher level components $\textit{M}$ from instantiating lower level subcomponents $\textit{M}_\textit{i} \in \textit{M}_\textit{M}^{*}=\{\textit{M}_{0}, \ldots , \textit{M}_\textit{j}\}$, $j \in {\mathbb {N}}$. These subcomponents’ behaviors can interact via the directed ports of the components’ interface declaration $\textit{p}_\textit{i} \in \bigcup _\textit{m} \chi _{m}$, $\chi _{m}=\chi _{m}^\textit{in} \cup \chi _{m}^\textit{out}$, $m \in \{M\} \cup \textit{M}_\textit{M}^{*}$. Its input ports are given by $\textit{x}_\textit{i} \in \chi _{m}^\textit{in}=\{\textit{x}_0, \ldots , \textit{x}_j\}$, $j \in {\mathbb {N}}$ and its output ports are given by $\textit{y}_\textit{i} \in \chi _{m}^\textit{out}=\{\textit{y}_0, \ldots , \textit{y}_j\}$, $j \in {\mathbb {N}}$. Their interconnection is denoted by directed nets $\textit{n}_\textit{i} = (\textit{p}_\textit{src}, \textit{p}_\textit{snk}) \in \textit{N}_\textit{M} = \textit{N}_\textit{M}^\textit{A} \cup \textit{N}_\textit{M}^\textit{D} = \{\textit{n}_0, \ldots , \textit{n}_j\}$, $j \in {\mathbb {N}}$. Among these, the assembly nets $\textit{n}_\textit{i} \in \textit{N}_\textit{M}^\textit{A} = \{ \textit{n}_\textit{i} | (\textit{p}_\textit{src} \in \chi _{\textit{M}_\textit{M}^{*}}^\textit{out}) \wedge (\textit{p}_\textit{snk} \in \chi _{\textit{M}_\textit{M}^{*}}^\textit{in}) \}$ denote the connections between the different subcomponents $\textit{M}_\textit{M}^{*}$ of $\textit{M}$. In contrast, the delegation nets $\textit{n}_\textit{i} \in \textit{N}_\textit{M}^\textit{D} = \{ \textit{n}_\textit{i} | ((\textit{p}_\textit{src} \in \chi _{\textit{M}}^\textit{in}) \wedge (\textit{p}_\textit{snk} \in \chi _{\textit{M}_\textit{M}^{*}}^\textit{in})) \vee ((\textit{p}_\textit{src} \in \chi _{\textit{M}_\textit{M}^{*}}^\textit{out}) \wedge (\textit{p}_\textit{snk} \in \chi _{\textit{M}}^\textit{out})) \}$ denote the connections between subcomponents $\textit{M}_\textit{M}^{*}$ and the composed component $\textit{M}$. Assuming both, the behavior of the components as well as their communication, to be compositional, a top-down refinement resp. bottom-up virtual integration of the composed behavior becomes possible, reducing the design complexity by a – possibly hierarchical – structural decomposition.

Hence, we consider a component M as $M = (\textit{tp}(M), \chi _M, S_M, D_M, B_M )$, with $\chi _M$, $S_M$, $D_M$, $B_M$ being tuples or sets and $\textit{tp}({M})$ denoting a function to resolve the component’s type name. For the top-level of a decomposition the type is also considered to represent the component’s instance name, normally given by for the lower levels of a decomposition. Similar to the notation in Sect. 2, the component’s port interface is defined by the set $\chi _M = \chi _M^{\textit{in}} \cup \chi _M^{\textit{out}}$ of input ports $x_i \in \chi _M^{\textit{in}}$ and output ports $y_i \in \chi _M^{\textit{out}}$. Besides a function $\textit{id}(\cdot )$ to resolve a port’s name, the declaration of each port $(\cdot )$ defines also functions $\nu (\cdot )$ to resolve its value domain – e. g. boolean or integer – and $\textit{dir}(\cdot ) \in \{\textit{in}, \textit{out}\}$ to resolve its direction as input resp. output.

Using an extended linear temporal logic, contracts $C_i:=(A_i, G_i)$ are used, to formally specify the assumptions $A_i$ of a component M w. r. t. to the timed behavior of its environment E, combined with its guarantees $G_i$, provided for the case that the corresponding assumptions $A_i$ are satisfied. To this end, the assumptions describe expressions, which observe (read) only the input variables, while the guarantees are expressions, which control (write) only the output variables. Semantically, both expressions are interpreted as sets $[\![\text {A}]\!]$ resp. $[\![\text {G}]\!]$ of timed traces $s_{x_i}$ resp. $s_{y_i}$ with $[\![A]\!]=\{(s_{x_0}, \ldots , s_{x_j}) | (\bigcup _{i=0}^{j} x_i = \chi _{M}^{in}) \wedge ([\![A]\!] \models A)\}$, $[\![G]\!]=\{(s_{y_0}, \ldots , s_{y_j}) | (\bigcup _{i=0}^{j} y_i = \chi _{M}^{out}) \wedge ([\![G]\!] \models G)\}$, satisfying the corresponding assertions A resp. G, and with $s_{x_i}=\{e_0(x_i), e_1(x_i) \ldots \}$ resp. $s_{y_i}=\{e_0(y_i), e_1(y_i) \ldots \}$ describing the timed traces of $x_i$ resp. $y_i$ as possibly infinite sequences of events $e_{\iota }(x_i) = (v(x_i), t_{\iota })$ resp. $e_{\iota }(y_i) = (v(y_i), t_{\iota })$ with variable value $v(x_i) \in \nu (x_i)$ resp. $v(y_i) \in \nu (y_i)$, time $t_{\iota }: (t_{\iota } \in {\mathbb {R}}_0^{+}) \vee (t_{\iota } \in {\mathbb {N}})$ and $\iota \in {\mathbb {N}}_0^{+}$. Using the contracts’ saturated interpretation $(A_i \rightarrow G_i^{'})$, with $G_i^{'}:=(A_i^{'} \rightarrow G_i)$ and $A_i^{'} \subseteq A_i$, compositional assume/guarantee reasoning becomes possible to prove the compatibility and refinement within a component based decomposition.

Thus, we provide the component’s contract based specification $S_M = \bigcup _i C_i$, which we onwards denote as behavioral specification. Accordingly, $B_M$ describes the corresponding behavioral implementation, e. g. given as an executable program, automata or formula. Furthermore, the tuple $D_M = (M_M^*, N_M)$ describes the component’s structural decomposition, either for the purpose of a structural top-down refinement of the initial specification as well as for the structural bottom-up implementation by instantiation and integration of available components. Finally, the norm $|\cdot |$ shall for all sets denote their number of elements and, if necessary for unambiguousness, we prefix identifiers and symbols by component identifiers M or $M_i$, using a dot as delimiter, as e. g. $M_0.C_0$, $M_1.C_0$, etc. For simplicity we identify components, contracts and ports by names equal to their symbols, so that , , , etc.

5 Structural Contracts

In general, being based on interface theories, Contract Based Design is limited to such specifications $S_M$, declaring only the externally observable ‘behavioral properties’ of the component – meaning ‘behavioral’ in that sense, that its properties refer only to the components’ explicitly declared ports. Differently, the component’s inherently contained ‘structural properties’ can neither be specified nor verified that way – meaning ‘structural’ not necessarily w. r. t. the physical but w. r. t. the logical structure, such as available ports, the instantiated subcomponents or the interconnection of a structural decomposition $D_M$ etc. As a solution, we suggest an introspection and reflection of these structural properties to introduce a structural point of view, enabling for structural contracts. According to the interface declaration $(\chi _M^\textit{in}, \chi _M^\textit{out})$ and the formal decomposition $D_M$ we extract the available structural information and systematically add an implicit interface $\chi _M^\textit{struc}$ of structural ports, which provide explicit access to the structural information. As a result, the component’s decomposition structure becomes specifiable and verifiable via contract based constraints for its original interface declaration, structural decomposition resp. the instantiation and integration of the component within a hierarchical composition.

To explain our approach in detail, we follow its sequential steps according to:

$$\begin{aligned} \begin{array}{ll} \text {1. extract structural information} &{} \text {4. add introspection components}\\ \text {2. build structural data types} &{} \text {5. add introspection subnets}\\ \text {3. insert introspection ports} &{} \text {6. add }structural\, guarantee \end{array} \end{aligned}$$

First, the components’ structural information ($\textit{tp}(M), \chi _M, S_M, D_M, B_M$) are derived from the component model, to build the data structure of M according to Sect. 4. In the second step – to avoid complete string analysis for the first approach – we generate structural data types according to the following enumerations:

$dt\_cId:$ :

set of all components identifiers tp(M) and $id(M_i)$ $\forall M_i \in M_M^{*}$

plus one additional ’open’ symbol to denote ports without a connection

$dt\_pId:$ :

set of all port identifiers $id(p_i) \in \chi _m$ of M and $M_i \in M_M^{*}$

plus one additional ‘open’ symbol to denote ports without a connection

Based on these structural data types, we then introduce the structural introspection ports according to Fig. 3. That is, for each port $p_i \in \chi _{M_i}$ of each subcomponent $M_i \in M_M^{*}$ of the decomposition $D_M$ two additional input ports of type $dt\_cId$ resp. dt_pId are added. For each input port $p_i = x_i \in \chi _{M_i}^{\textit{in}}$ the ports are named $M_i.id(x_i)\_cSrc$ and $M_i.id(x_i)\_pSrc$ resp. $M_i.id(y_i)\_cSnk$ and $M_i.id(y_i)\_pSnk$ for each output port $p_i = y_i \in \chi _{M_i}^{\textit{out}}$. Using these additional ports the components are enabled to receive information about the connections between their original ports, meaning the identifiers of the ‘source component’ and ‘source port’ resp. the ‘sink component’ and ‘sink port’ connected via the net $n_i$, resp. to receive ‘open’ if ports remained unconnected.

Fig. 3.

Overview of the implicitly inserted structural introspection ports, extending the port interface of each subcomponent within a decomposition $D_M$ of a component M.

In the fourth step, an additional introspection component $M_\textit{DM}$ is added to the decomposition structure – i.e. $M_M^{*} := M_M^{*} \cup M_\textit{DM}$ – to reflect the component’s structural information via the introspection ports. To this end, $M_\textit{DM}$ provides the structural output ports $M_\textit{DM}.id(M_i.x_i)\_cSrc$, $M_\textit{DM}.id(M_i.x_i)\_pSrc$, $M_\textit{DM}.id(M_i.y_i)\_cSnk$ and $M_\textit{DM}.id(M_i.y_i)\_pSnk$, building the corresponding counter part to the structural ports we introduced in step three.

Fig. 4.

Extension of a component’s decomposition $D_M$ by an introspection component $M_\textit{DM}$ and structural nets $n_\textit{cSrc}(n_i)$, $n_\textit{pSrc}(n_i)$, $n_\textit{cSnk}(n_i)$, $n_\textit{pSnk}(n_i)$, connecting the introspection component with the subcomponents.

In the fifth step, we complete the communication structure of the structural view according to Fig. 4, connecting the structural introspection ports of $M_\textit{DM}$ with the corresponding subcomponents $M_i \in M_M^{*}$. To this end, for all nets $n_i \in N_M$ additional subnets $N_\textit{DM}=\bigcup _{n_i} n_\textit{cSrc}(n_i) \cup \bigcup _{n_i} n_\textit{pSrc}(n_i) \cup \bigcup _{n_i} n_\textit{cSnk}(n_i) \cup \bigcup _{n_i} n_\textit{pSnk}(n_i)$ are inserted to $N_M$, according to the following rules:

$$\begin{aligned} n_\textit{cSrc}(n_i)&= (M_\textit{DM}.id(M_i.x_i)\_cSrc, M_i.id(M_i.x_i)\_cSrc),\\ n_\textit{pSrc}(n_i)&= (M_\textit{DM}.id(M_i.x_i)\_pSrc, M_i.id(M_i.x_i)\_pSrc),\\ n_\textit{cSnk}(n_i)&= (M_\textit{DM}.id(M_i.y_i)\_cSnk, M_i.id(M_i.y_i)\_cSnk),\\ n_\textit{pSnk}(n_i)&= (M_\textit{DM}.id(M_i.y_i)\_pSnk, M_i.id(M_i.y_i)\_pSnk). \end{aligned}$$

Finally, the introspection component $M_\textit{DM}$ is annotated with structural guarantees $C: ( (A: \textit{true}), (G: \langle {struc\_port} \rangle = \langle {struc\_value} \rangle ) )$, reflecting the information of the original component’s interconnections with ${struc\_value} \in \nu (struc\_port)$ and:

Differently, for the subcomponents $M_i \in M_M^{*}$ the corresponding structural introspection ports allow to constrain the components’ interconnections by structural assumptions $C: ( (A: \langle {struc\_port} \rangle = \langle {struc\_value}^{*} \rangle ), (G: \textit{true}) )$, with ${struc\_value}^{*} := \{ \langle {struc\_value} \rangle | \langle {struc\_port} \rangle \}$, ${struc\_value} \in \nu (struc\_port)$ and:

That way, the structural information of a decomposition are treated as properties, which are provided from the compositional environment which embedds the instantiated components, consequently allowing for a contract based assume-guarantee reasoning in this structural view. Following from this, structural assumptions can be specified top-down, becoming part of the functional and extra-functional contracts and thus an additional validity constraints during the compatibility and refinement checking within multiple viewpoints.

6 Proof of Concept

For a first proof of concept, we evaluated our approach of structural contracts for the motivating example, outlined in Sect. 2. To this end, we implemented the component interfaces of M and its subcomponents $M_0$, $M_1$ and $M_2$ and provided them with contracts according to the functional and extra-functional properties given in Table 1. Based on this implementation we showed that structural contracts are able to reveal the false negative verification of the erroneous logical structure depicted in Fig. 2. Furthermore, we showed that for a correct structural decomposition our structural extension does not influence compatibility and refinement checking of the other functional and extra-functional properties. For the implementation and evaluation we used OTHELLO (Object Temporal with Hybrid Expressions Linear-Time LOgic) [8] for the specification of contracts and OCRA (OTHELLO Contracts Refinement Analysis) [7] to describe the components as OSS (OCRA System Specification) [7] and to check their compatibility and their refinement. To reproduce our study, our example is online available at [10].

7 Conclusion

Based on an artificial example we motivate the need for structural contracts and show how structural contracts increase the reliability of composed extra-functional multi-domain models. By the evaluation of the example we show that structural contracts can reveal failures in the logical composition structure, which otherwise remain hidden, enabling false negatives during extra-functional verification.

In the future work, we want to investigate the abstraction and refinement of our structural contracts and evaluate how structural contracts can be propagated throughout the design and abstraction hierarchies. Furthermore, we plan to examine if and which additional port annotations will become necessary enable this hierarchies and to allow for the seamless and composable integration of designer-defined extra-functional semantics based on structural contracts.