The management of modern enterprise applications is automated by coordinating the deployment, configuration, enactment, and termination of their components. Choosing among different candidate implementations for a specified application component requires such implementations to conform to the specified management behaviour. This holds especially if we wish to ensure that the overall application management can continue as planned, or that no additional (potentially undesired) management activity gets enabled. To this end, we introduce a formal framework for testing “management conformance”, i.e., to test whether a candidate implementation can be managed according to the management protocol specifying the allowed management for a component. We also illustrate how our framework enables to run four different conformance tests, each providing a different trade-off between implementation freedom and guarantees on the overall application management. We formally prove that testing management conformance with constraints reducing implementation freedom results in preserving all already allowed management activities when implementing a specification by choosing a conforming implementation and that no additional (potentially undesired) management activity gets enabled. Finally, we assess our framework by means of a prototype implementation and its use in an experimental evaluation.
Notes
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
Modern enterprise applications (e.g., cloud-native applications) integrate multiple heterogeneous components, therein included the software services running an application’s business logic and the infrastructure components they need to run [1]. Managing such applications hence requires suitably coordinating the deployment, configuration, and operation of their components [2]. This must be done by considering various dependencies and interconnections occurring among the components forming an application, and the possibility of such components to fail [3].
Topology graphs [4] and management protocols [5] support such a dependency- and fault-aware automation, by enabling to specify the structure of applications and their allowed management. Topology graphs [4] enable specifying the topology (i.e., the structure) of an application as a directed graph, whose nodes represent application components. Directed arcs represent inter-component dependencies, by connecting a component’s requirement to a capability offered by another component. Management protocols [5] then exploit the relation between nodes’ requirements and capabilities to enable modelling the allowed management behaviour of each node, e.g., when its management operations can be invoked, which are their effects, or how it reacts to the faults due to their requirements stopping to be satisfied (despite actually needed to reside in a state or to perform some management operations).
Advertisement
At the same time, application administrators typically may wish to concretely implement specified application components by choosing among different candidate implementations [6]. The latter may even possibly be “black-box” implementations delivered by different service providers. For a candidate implementation to suitably implement a given specification, such implementation should also conform to the management behaviour specified by its management protocol. This means that the chosen implementation can be managed by executing the specified operations in the specified order, that it properly interacts with the other components forming an application, and that it handles potential faults as specified. Hence, a notion of “management conformance” can enable application administrators to implement a specified component by choosing candidate implementations that can be managed as specified, by also providing guarantees on the way the implemented component interacts with the rest of the application.
With the ultimate goal of enabling to check such a management conformance, we hereafter introduce a framework for management conformance testing based on management protocols [5] and Tretmans’ input/output (I/O) conformance testing [7]. Our framework is the first combining I/O conformance testing [7] with management protocols [5] to check—at design-time—whether a candidate implementation can be used to implement the specification of a desired component, while ensuring that the chosen implementation can be managed as specified, also in the presence of possible faults. It also enables considering how the chosen implementation can interact with the rest of the application when coordinating the whole application management.
Following Tretmans’ I/O conformance testing [7], we first introduce an encoding of management protocols for expressing their semantics in terms of I/O labelled transition systems (IOLTS). We then exploit the IOLTS encoding of management protocols to define a parametric relation for testing management conformance. The parametric relations can be instantiated to obtain four different management conformance testing operators, which enable checking whether candidate implementations can be chosen to concretely implement the specification of a desired component.
We also formally illustrate how the obtained testing operators constitute different trade-offs among implementation freedom and guarantees obtained by choosing a conforming implementation to concretely implement a component specification. More relaxed testing operators enable, for instance, component specifications to exhibit a non-deterministic management behaviour, hence leaving freedom in choosing which branches of such behaviour to actually implement. Stricter testing operators instead reduce implementation freedom, while enforcing guarantees on the overall application management, i.e., ensuring that by choosing a conforming implementation to implement a component specification preserves allowed management activities, or that no (potentially undesired) management activity gets enabled.
Advertisement
Finally, to assess practical applicability of the proposed framework for testing management conformance, we introduce a prototype implementation, based on specifying applications with the OASIS standard TOSCA [8]. We also show how we used such prototype to experiment our framework.
The main contributions of this article can be summarised as follows:
(a)
We provide an IOLTS encoding for management protocols modelling the management behaviour of application components.
(b)
We present a parametric relation for testing whether the management protocol of an available implementation conforms to that of a component specification, which enables instantiating four different management conformance testing operators.
(c)
We establish and formally prove compositionality properties resulting from testing conformance with different operators, i.e., whether operators ensure that the overall application management is preserved when choosing a conforming implementation to implement a component specification, or that no undesired management activities get enabled.
(d)
We present a prototype implementation of the proposed management conformance testing and we discuss how we used it an experimental evaluation.
This article extends our previous work [9]. Contributions (c) and (d) are indeed brand new and first presented in this article.
The article is organised as follows. Sections 3 and 2 provide an overview of our framework and the necessary background on fault-aware management protocols, respectively. Section 4 introduces our framework for testing management conformance. Section 5 introduces and proves the compositionality results for management conformance testing. Section 6 presents the prototype implementation and its use in realistic experiments. Finally, Sections 7 and 8 discuss related work and draw some concluding remarks, respectively.
2 Motivations
We hereafter give an intuitive overview of the rationale and steps to be followed for using the proposed framework for management conformance testing framework. We also introduce a scenario, which we then use as running example in the presentation of our framework.
2.1 Overview
Modern enterprise applications integrate multiple heterogeneous components [1]. Some components may already come with a concrete implementation. The remaining components are instead only specified in the overall application design, considering how they interact with the rest of the application, yet requiring a concrete implementation to be looked for [10]. Our framework comes to this purpose, by enabling to choose—at design-time—among multiple possible candidate implementations specified components.
For each specified component, the process to follow is that in Fig. 1. We start from the component specification, which comprises the allowed management behaviour (step 1). To test whether a candidate implementation conforms to such specified management, we should then differently proceed depending on whether the test setting is white-box or black-box. In a white-box setting, we have full access to the internal details and sources of candidate implementations, hence knowing the management protocol specifying the actual management of the available implementation (step 2a). Instead, in a black-box setting, we should equip the candidate implementation with an interface enabling to invoke their management operations, satisfy their requirements, and observe their capabilities (step 2b). We could then test management conformance with the framework proposed in this article (step 3).
Fig. 1
Steps for testing the management conformance of a candidate implementation to each specified component
×
2.2 Running example
Fig. 2
Example of application topology, depicted according to the TOSCA graphical notation [11]
×
The clients of the application connects to the gui, which relies on the backend api to serve them. The api accesses the database for managing application data. Figure 2 illustrates the topology of such an application, whose nodes model the application components, and their requirements, capabilities, and management operations. Connections are modelled as directed arrows connecting a node’s requirement to another node’s capability. The connection from gui to api is represented by indicating that the requirement endp of api is satisfied by the homonym capability of api. Similarly, the connection from api to database is represented by indicating that the requirement db of api is satisfied by the homonym capability of database.
Suppose that gui and database are already implemented, while api is only specified. Suppose also that we specified that the desired management for api is that specified by the management protocol [5] in Fig. 3a (step 1 of Fig. 1), since we considered it to devise management plans coordinating the overall application management.
Fig. 3
Examples of management protocols for the node api in Fig. 2
×
The management protocol in Fig. 3a specifies the possible states of api, i.e., unavailable (initial), installed, started, and failed. Operation transitions indicate how api can move from a state to another by executing the corresponding operation, with configure self-looping on state installed. The management protocol indicates that the requirement db is needed to reside in states installed and started, with the latter being also the only state where api is providing its capability endp. The requirement db is also needed to perform the self-looping transition corresponding to the operation configure. No requirement is instead needed by api to reside in any other state or to execute any other operation. Finally, fault-handling transition illustrate how api reacts to the fault of the requirement db when it is installed or started. If db stops being satisfied while api is in one of such states (because database stops providing the capability db used to satisfy such requirement), api gets failed.
Consider now the problem of concretely implementing the api component, e.g., by choosing among already existing, candidate implementations. To simplify presentation, we consider a white-box setting, assuming to have full access to a candidate implementation of api, and knowing that it can be managed according to the management protocol in Fig. 3b (step 2a in Fig. 1). Can we choose such candidate implementation to concretely implement the specified api component? If yes, which guarantees do we have when choosing it for implementing api? We now show how to answer the above questions by running the step 3 in Fig. 1 with our proposed management conformance testing framework.
3 Preliminaries
Management protocols [5] enable analysing and automating the management of multi-component applications, under the control of an orchestrator coordinating the invocation of the management operations of the components therein.1 We hereafter recap the basics on management protocols [5] needed to formally introduce our management conformance testing framework.
3.1 Management protocols
Topology graphs allow representing the components forming an application and the dependencies occurring among them [4]. Application components are represented as nodes, each describing the requirements of the corresponding component, the operations to manage it, and the capabilities it features to satisfy other components’ requirements. Arcs model dependencies by associating each requirement of each node with the capability of another node used to satisfy such requirement.
Management protocols [5] enable to specify the management behaviour of a node N by indicating whether/how each management operation of N depends on other operations of N or of the nodes providing capabilities used to satisfy its requirements, as well as how N reacts when a fault occurs. The dependencies among the management operations of N are indicated by a finite state machine, whose transition relation \(\tau _N\) relates the management operations of N with its states. The transition relation indicates whether an operation o can be executed in a state s of N, and which state is reached by executing o in s.
The description of whether and how the management operations of N depends on those of other nodes is given by enriching the finite state machine with conditions associating (possibly empty) sets of requirements and capabilities with both transition and states. The requirements associated with a transition must be satisfied to allow its execution, while those associated with a state must continue to be satisfied in order for N to continue to work properly. The capabilities associated with a transition/state are those offered by N during such transition/state.
Finally, management protocols also allow to indicate how N reacts when a fault occurs, i.e., when N is in a state assuming some requirements to be satisfied, but some other node stops satisfying such requirements. This is specified by another transition relation \(\varphi _N\), which models the fault handling of N by specifying that its state changes from s to \(s'\) when some of the requirements it assumes in s stop being satisfied.2
Definition 3.1
(Management Protocol) Let \(N = \langle S_N, R_N, C_N, O_N, \mathcal {M}_N \rangle \) be a node, where \(S_N\), \(R_N\), \(C_N\), and \(O_N\) are the finite sets of its states, requirements, capabilities, and management operations (with \(S_N \ne \varnothing \) and \(O_N \ne \varnothing \)). \(\mathcal {M}_N = \langle {\overline{s}}_N, \rho _N, \chi _N,\)\(\tau _N, \varphi _N \rangle \) is a finite state machine defining the management protocol of N, where:
\({\overline{s}}_N \in S_N\) is the initial state,
\(\rho _N : S_N \rightarrow 2^{R_N}\) is a function indicating, for each state \(s \in S_N\), which conditions on requirements must hold,
\(\chi _N : S_N \rightarrow 2^{C_N}\) is a function indicating which capabilities of N are concretely offered in a state \(s \in S_N\),
\(\tau _N \subseteq S_N \times 2^{R_N} \times 2^{C_N} \times O_N \times S_N\) is a set of quintuples modelling the transition relation,
\(\varphi _N \subseteq S_N \times S_N\) is a set of pairs modelling the fault handling for a node.
Remark 3.1
\(\langle s, R, C, o, s' \rangle \in \tau _N\) denotes that in state s, and if condition \(P\) holds, o can be executed and leads to state \(s'\), by maintaining the capabilities in C during the transition. Instead, \(\langle s, s' \rangle \in \varphi _N\) denotes that the node will change its state from s to \(s'\) if some of the requirements in \(\rho _N(s) - \rho _N(s')\) stop being satisfied.
We hereafter assume management protocols to be complete (i.e., handling all possible faults in all possible states) and race-free (i.e., handling faults so that the simultaneous removal of a set of requirements has the same effect on a node as any sequential removal of the same requirements). The construction rules for ensuring both properties on any management protocol can be found in [5].
3.2 Application management
To show how to derive the management behaviour of an application by composing the management protocols of its components, we first introduce a shorthand notation to denote applications. This simplifies eliciting the nodes in an application’s topology and the connections among their requirements and capabilities.3
Notation 3.1
We denote with \(A = \langle T, b\rangle \) a generic multi-component application, where T is the finite set of nodes in the application topology, and where the connections among nodes is described by a (total) binding function
associating each requirement of each node with the capability used to satisfy such requirement.
The semantics of the management protocols in a multi-component application \(A = \langle T, b\rangle \) is defined by a labelled transition system over configurations that denote the states of the nodes in T. Intuitively, \(G\xrightarrow {o} G'\) is a transition denoting that operation o can be executed (on a node) when the “global” state of A is \(G\) and that it makes A evolve into the new global state \(G'\). We hence first recall from [5] the notion of global state, which is defined as a set \(G\) containing only the current state of each of the nodes forming an application.
Definition 3.2
(Global State) Let A=\(\langle T, b\rangle \) be an application, and let us denote with \(\langle S_N, R_N, C_N,\)\(O_N, \mathcal {M}_N \rangle \) the tuple corresponding to a node \(N \in T\). A global state G of A is a set of states such that:
\(\overline{G}\) denotes the initial global state of an application A=\(\langle T, b\rangle \), where each node is in its initial state (viz., \(\overline{G}= \bigcup _{N \in T} {\overline{s}}_N\)).
We also recall the function \(F\) denoting the set of pending faults in \(G\), i.e., requirements assumed in \(G\), even if bound to capabilities not provided in \(G\). To do so, we exploit some shorthand notations to indicate the requirements and capabilities associated with a global state, and the set of capabilities bound to a given set of requirements.
Notation 3.3
Let \(G\) be a global state of an application \(A = \langle T, b\rangle \). We denote with \(\rho (G)\) the requirements that are assumed to hold by the nodes in T when A is in \(G\), with \(\chi (G)\) the capabilities provided by such nodes in \(G\), and with \(b(R)\) the capabilities bound to the requirements in R:
(Pending faults) Let \(A = \langle T, b \rangle \) be an application, and let \(G\) be a global state of A. The set \(F(G)\) of pending faults in \(G\) is defined as:
The management behaviour of an application is then given by a labelled transition system, whose configurations are the global states of A. The transition system is characterised by two inference rules, i.e., op for operation execution and fault for fault propagation. The former permits executing a management operation o on a node \(N \in T\) only if there are no pending faults and all the requirements needed by N to perform o are satisfied (by the capabilities provided by other nodes in T).4 The latter illustrates how to handle pending faults.
Definition 3.4
(Application Behaviour) Let \(A \, \text {= } \, \langle T, b \rangle \) be an application, and let us denote with \(\langle S_N, R_N, C_N, O_N, \mathcal {M}_N \rangle \) the tuple corresponding to a node \(N \in T\). Let also \(\mathcal {M}_N = \langle {\overline{s}}_N, \rho _N, \chi _N,\)\(\tau _N, \varphi _N \rangle \). The management behaviour of A is modelled by a labelled transition system whose configurations are the global states of A:
4 Testing management conformance
To align with Tretmans’ idea of I/O conformance testing [7], management conformance is defined on IOLTS encodings of the formalism under consideration. We hence first introduce an encoding of management protocols into IOLTSs (Section 4.1) and characterise its suitability for conformance testing (Section 4.2). We then exploit the IOLTS encoding of management protocols to formally introduce management conformance testing in multi-component applications (Section 4.3).
4.1 IOLTS encoding
With the ultimate goal of defining an IOLTS encoding for the management protocol of a node \(N = \langle S_N, R_N, C_N, O_N, \mathcal {M}_N \rangle \), we first identify the input and output actions for N. The possible input actions for N are of two different types, i.e., operation-invocation actions and requirement-set actions. An operation-invocation action \(\textit{o}^\uparrow \) denotes the invocation of an operation \(o \in O_N\) in a state. A requirement-set action R (with \(R \in R_N\)) instead denotes a subset of the requirements of N that are satisfied by capabilities provided by other components in the application. They are modelled as input actions, since they are both provided by external entities: Operation invocation is indeed performed by the application orchestrator, while requirements are satisfied by capabilities provided by other components in the applications.
The output actions instead enable observing the outputs possibly generated by N after executing some input action, namely whether an invoked operation completed, which capabilities it provides, or whether some fault occurred. An operation-termination action \(\textit{o}^\downarrow \) notifies the completion of a previously invoked operation \(o \in O_N\). A capability-set action C (with \(C \in C_N\)) denotes a subset of the capabilities of N that are provided by N to the rest of the application. Finally, fault-handling actions enable explicitly observing the activation of fault handlers, by means of a special output symbol \(\bot \not \in (R_N \cup C_N \cup O_N)\).
Definition 4.1
(Input/Output Actions) Let \(N = \langle S_N, R_N, C_N,\)\(O_N, \mathcal {M}_N \rangle \) be a node. The set \(\textit{Act}_{N}\) of possible I/O actions for N is defined as \(\textit{Act}_{N} = \textit{In}_{N} \cup \textit{Out}_{N}\), where
\(\textit{In}_{N} = \{ \textit{o}^\uparrow \mid o \in O_N \} \cup 2^{R_N}\) and
The set of possible I/O actions for a node N defines the labelling alphabet for the IOLTS encoding its management protocol \(\mathcal {M}_N = \langle {\overline{s}}_N, \rho _N, \chi _N, \tau _N, \varphi _N \rangle \) of a node N. The configurations \(X_N\) of the IOLTS encoding of \(\mathcal {M}_N\) are then given by the set of states \(S_N\) of N, extended by a set of fresh configurations denoting the execution of operation transitions and fault-handling transitions, i.e., \(X_N = (S_N \cup \tau _N) \cup \varphi _N\). The initial configuration of the IOLTS corresponds to the initial state of \(\mathcal {M}_N\), i.e., \({\overline{s}}_N\).
The transition relation of the IOLTS encoding of \(\mathcal {M}_N\) is obtained in three steps, to differently encode states, operation transitions, and fault-handling transitions.
(i)
The conditions on requirements and capabilities associated with each state \(s \in S_N\) are encoded by two IOLTS transitions self-looping on s. These are a requirement-set input transition encoding the requirements assumed by N in s, and a capability-set output transition encoding the capabilities provided by N in s.
(ii)
For each transition \(t = \langle s,R,C,o,s' \rangle \in \tau _N\) in the management protocol, four transitions are added to the corresponding IOLTS encoding. Two of such transitions encode the invocation and completion of the operation o, i.e., an operation-invocation input transition \(\textit{o}^\uparrow \) from s to t, and an operation-completion output transition \(\textit{o}^\downarrow \) from t to \(s'\). Two transitions self-looping on t instead encode the conditions on requirements and capabilities associated with t, i.e., a requirement-set input transition labelled with R, and a capability-set output transition labelled with C.
(iii)
Each fault handler \(f = \langle s, s' \rangle \in \varphi _N\) is encoded by adding two IOLTS transitions for each subset of the requirements assumed in s and handled by f: an input transition labelled with the set R of remaining requirements (i.e., the requirements that were assumed in s and that continue to be satisfied by the rest of the application) goes from s to f, modelling the reaction of N to the handled fault (i.e., the requirements in \(\rho _N(s) - R\)). An output transition labelled with \(\bot \) instead goes from f to \(s'\), hence enabling to explicitly observe the issuing of a fault handler.
Definition 4.2
(IOLTS Encoding) Let \(N=\langle S_{N}, R_{N}, C_{N}, O_{N}, {\mathcal {M}}_{N}\rangle \) be a node, with \(\mathcal {M}_N = \langle {\overline{s}}_N, \rho _N, \chi _N, \tau _N, \varphi _N \rangle \). The IOLTS encoding of the management protocol \(\mathcal {M}_N\) of N is defined as a triple \({\mathcal {I}}_N = \langle {\overline{s}}_N,X_N,\rightarrow _{N}\rangle \), where
IOLTS encoding of the management protocols in Fig. 3. Solid and dashed transitions correspond to input and output actions, respectively. Configurations corresponding to states of the original management protocols are in grey
×
The proposed encoding preserves the semantics of management protocols. While this can be directly observed on the encoding of conditions on capabilities, that of requirements and faults needs a small digression. It indeed exploits a peculiar aspect of I/O conformance testing, namely that all possible inputs should be testable. Even if some tests may skip the self-loops encoding the conditions associated with states and transitions, we must always test also the cases in which self-loops are included, therefore constraining the corresponding requirements to be satisfied for the component to reside in a state or to perform a transition. For the same reasons, the fault handler \(\langle s, s' \rangle \in \varphi _N\) is encoded by multiple transitions to model all possible sets of faults it handles (viz., all possible subsets of \(\rho _N(s) - \rho _N(s')\)).
Figure 4 shows the IOLTS encodings of the management protocols in Fig. 3. The configurations of both IOLTSs are given by the union of the sets of states, operation transitions, and fault-handling transitions of the original management protocols. Intermediate configurations are used to split each operation transition into an operation-invocation input transition and an operation-completion output transition. For instance, the operation transition leading from unavailable to installed with the operation install is split into two IOLTS transitions \(\textsf {install} ^\uparrow \) and \(\textsf {install} ^\downarrow \).
Fault-handling transitions in management protocols are also split into two IOLTS transitions. Consider the configuration started, whose corresponding state assumes db to be satisfied. If no requirement is given as input, this means that db stops being satisfied and the configuration of the IOLTS changes from started to failing, from which (the configuration corresponding to) state failed can be reached by producing the output \(\bot \). The two transitions in the IOLTS model the corresponding fault-handling transition in the original management protocol.
Finally, self-loops model the conditions on requirements and capabilities associated with states and transitions. For instance, the configuration started has two self-loops. The dashed self-loop models the fact that the node is offering the capability endp while residing in state started, since it can produce \(\textsf {\{}\textsf {endp} \textsf {\}}\) as output. The solid self-loop instead indicates that the node keeps residing in state started if the requirement db continues to be satisfied, since the configuration does not change when \(\textsf {\{}\textsf {db} \textsf {\}}\) is given as input.
4.2 Input-enabledness
I/O conformance testing requires candidate implementations to be input-enabled: any candidate implementation should never block on any input action during testing, so that for every test execution a definitive pass/fail verdict can be made [7]. We consider a management protocol as input-enabled if its IOLTS encoding accepts any possible input in any configuration corresponding to a state in the management protocol.
Notation 4.1
Let \({\mathcal {I}}_N = \langle {\overline{s}}_N,X_N,\rightarrow _{N}\rangle \) be the IOLTS encoding of the management protocol of a node N. Given a configuration \(x \in X_N\), we use \(x\xrightarrow {\sigma }_{N}x'\) and \(x\xrightarrow {\sigma }_{N}\) (with \(\sigma \in \textit{Act}_{N}^{*}\)) to denote traces \(\sigma \) corresponding to valid paths from x in \({\mathcal {I}}_N\).
Definition 4.3
(Input-Enabledness) Let \({\mathcal {I}}_N = \langle {\overline{s}}_N,X_N,\rightarrow _{N}\rangle \) be the IOLTS encoding of the management protocol of a node N. \({\mathcal {I}}_N\) is input-enabled iff \( \forall x \in S_N\, .\, \forall i\in \textit{In}_{N}:{x\xrightarrow {i}_N\!.}\)
Consider again the IOLTSs in Fig. 4, which encode the (a) management protocol specification and (b) candidate implementation for the component api in our running example (Fig. 3). One can readily observe that both IOLTSs are such that the corresponding management protocols are not input-enabled, as there exist configurations corresponding to state of the corresponding management protocol that lack some outgoing input transitions (e.g., there is only one out of the five possible operation-invocation actions defined for started). As I/O conformance testing requires implementations to be input-enabled [7], to be able to test whether the candidate implementation of api conforms to its specification, its management protocol should be input-enabled.
The input-enabledness of a management protocol can be ensured automatically. Intuitively, its IOLTS encoding can be completed by adding an input transition targeting a distinct sink configuration \(s_\bot \) (with \(s_\bot \notin X_N\)) for each unspecified input of each state \(s\in S_N\), i.e., a requirement-set input transition labelled with R is added if there is no such transition outgoing from s, and an operation-invocation input transition labelled with o if o cannot be invoked in s. The sink state \(s_\bot \) is also input-enabled by adding a self-looping input transition for each possible input.
In addition, a self-looping output transition on \(s_\bot \) is added and labelled with the special symbol \(\bot \). This enables observing that an unspecified input has been provided to the IOLTS, as when this happens the IOLTS can provide \(\bot \) as output.
Definition 4.4
(Input Completion) Let \(N=\langle S_{N}, R_{N}, C_{N}, O_{N}, {\mathcal {M}}_{N}\rangle \) be a node, with \(\mathcal {M}_N = \langle {\overline{s}}_N, \rho _N, \chi _N, \tau _N, \varphi _N \rangle \). Let also \({\mathcal {I}}_N = \langle {\overline{s}}_N,X_N,\rightarrow _{N}\rangle \) be the IOLTS encoding of \(\mathcal {M}_N\). The input completion of \({\mathcal {I}}_N\) is given by the tuple \({\mathcal {I}}_N' = \langle {\overline{s}}_N,X_N',\rightarrow _{N}'\rangle \) where
By applying the above-listed construction rules to the IOLTS encoding of the management protocol of the candidate implementation of api (Fig. 4b), we can make such implementation input-enabled (Fig. 5).
Fig. 5
Input-enabled version of the IOLTS in Fig. 4b, obtained by input completion
×
4.3 Management conformance
Consider an application component, and suppose N to constitute the (fully known) specification of its intended management behaviour. Suppose also \(N'\) to constitute a candidate implementation for N, defined over the same sets of requirements, capabilities, and management operations. We hereafter formally define an I/O conformance relation on management protocols (\(\mathsf {mpioco}\)), such that \(N' \, \mathsf {mpioco}\, N\) denotes that the management behaviour implemented by \(N'\)conforms to that specified by N, i.e., given the same inputs, \(N'\) can produce the outputs specified by N. Intuitively, \(N' \, \mathsf {mpioco}\, N\) means that, if provided with the same requirements and operations, \(N'\) can offer the capabilities offered by N. This hence means that \(N'\) can be used to implement N in a multi-component application.
To define the \(\mathsf {mpioco}\) relation, we first formally introduce the notions of quiescence and suspension traces. Quiescence occurs in a state when no output can be provided [12]. As for the IOLTS encoding of a management protocol, quiescence occurs whenever a configuration corresponds to a state in the original protocol where no capability is provided. For explicitly observing quiescence, we introduce a special output symbol \(\delta \notin (R_N \cup C_N \cup O_N)\) denoting it. We then define suspension traces by extending existing traces by enabling to explicitly observe quiescence.
Definition 4.5
(Quiescence, Suspension Traces) Let \(N=\langle S_{N}, R_{N}, C_{N},O_{N}, {\mathcal {M}}_{N}\rangle \) be a node and let \({\mathcal {I}}_N = \langle {\overline{s}}_N,X_N,\rightarrow _{N}\rangle \) be the IOLTS encoding of \(\mathcal {M}_N\). Let also \(x \in X_N\) be a configuration in \({\mathcal {I}}_N\).
x is quiescent, denoted by \(\delta (x)\) iff
, and
\(\mathsf {straces}(x) = \{ \sigma \mid x \xrightarrow {\sigma }_N \}\), where
We also introduce the notion of enabled outputs to identify the set of output symbols enabled by a set of configurations. Intuitively, these correspond to the outputs that can be produced from any configuration in the set.
Definition 4.6
(Enabled Outputs) Let \(N=\langle S_{N}, R_{N}, C_{N},O_{N}, {\mathcal {M}}_{N}\rangle \) be a node and let \({\mathcal {I}}_N = \langle {\overline{s}}_N,X_N,\rightarrow _{N}\rangle \) be the IOLTS encoding of \(\mathcal {M}_N\). The set of outputs enabled in a configuration \(x \in X_N\) is the least set \(\mathsf {out}(x)\) such that
\(C \subseteq \mathsf {out}(x) \text { if } x\xrightarrow {C}_N\),
\(\{ \bot \} \subseteq \mathsf {out}(x) \text { if } x\xrightarrow {\bot }_N\), and
\(\mathsf {out}(X)\) denotes the outputs enabled in at least one of the configurations in the set \(X \subseteq X_N\), i.e., \(\mathsf {out}(X) = \bigcup _{x \in X} \mathsf {out}(x)\).
Finally, we introduce the notion of reachability, which enables identifying the configurations that can be reached by performing a trace \(\sigma \) in a configuration x. We define two different versions of reachability, distinguished by parameter \(\gamma \). If \(\gamma \) is “\(=\)”, the transitions involving a set of requirements or capabilities are considered only if the trace \(\sigma \) delivers exactly that set of requirements or capabilities. If \(\gamma \) is instead set to “\(\ge \)”, we obtain a more relaxed notion of reachability. Indeed, with \(\gamma \) set to “\(\ge \)”, a transition labelled with a set \(R'\) of requirements is considered if the trace is delivering at least the requirements in \(R'\), while one labelled with a set \(C'\) of capabilities is considered if the trace is delivering at most the capabilities in \(C'\). Operation-invocation and operation-completion transitions are instead always considered, independently of the value associated with \(\gamma \).
Definition 4.7
(\(\gamma \)-Reachability) Let \(N=\langle S_{N}, R_{N}, C_{N},\)\(O_{N}, {\mathcal {M}}_{N}\rangle \) be a node and let \({\mathcal {I}}_N = \langle {\overline{s}}_N,X_N,\)\(\rightarrow _{N}\rangle \) be the IOLTS encoding of \(\mathcal {M}_N\). Let also \(x \in X_N\) be a configuration in \({\mathcal {I}}_N\) and \(\sigma \in \mathsf {straces}(x)\) be a suspension trace for x. The set of \(\gamma \)-reachable configurations from x with \(\sigma \) is \(\mathsf {reach}_{\gamma }(x,\sigma ) \subseteq X_N\), i.e., the least set satisfying the following recursive rules:
where \(\alpha \cdot \omega \) denotes an I/O action \(\alpha \) followed by a sequence \(\omega \) of I/O actions.
The above-introduced notions set the foundations for formally defining how to test management conformance between a candidate implementation and the specification of an application component. This can be done by means of the parametric relation (\(\mathsf {mpioco}\)) for testing management conformance defined hereafter, which enables obtaining four different conformance testing operators. The latter distinguished based on (a) the employed notion of \(\gamma \)-reachability and on (b) the way non-deterministic output-behaviour is handled. Concerning (b), we introduce some shorthand notations for comparing sets of sets, i.e., we write \(Z' \sqsupset Z''\) to indicate that \(Z''\) contains all sets in \(Z'\), and \(Z' \sqsupseteq Z''\) to indicate that \(Z''\) contains a superset of each set in \(Z'\).
Notation 4.3
Let \(Z'\) and \(Z''\) be two sets, whose elements are in turn sets. We write \(Z'\sqsupset Z''\) iff \(\forall z'\in Z':(\exists z''\in Z'':z''= z')\), and \(Z'\sqsupseteq Z''\) iff \(\forall z'\in Z':(\exists z''\in Z'':z''\supseteq z')\).
Definition 4.8
(\(\mathsf {mpioco}\)) Let N=\(\langle S_{N},R_{N},\)\(C_{N}, O_{N}, {\mathcal {M}}_{N}\rangle \) be a node, with \(\mathcal {M}_N\)=\(\langle {\overline{s}}_N, \rho _N,\)\(\chi _N, \tau _N, \varphi _N \rangle \). Let \(N'=\langle S_{N}', R_{N}, C_{N}, O_{N}, {\mathcal {M}}_{N}'\rangle \) be another node, with \(\mathcal {M}_N = \langle {\overline{s}}_N', \rho _N', \chi _N', \tau _N', \varphi _N' \rangle \) being input-enabled. Let also \(\beta \in \{ \sqsupset , \sqsupseteq \}\) and \(\gamma \in \{ =, \ge \}\). \(N' \, \mathsf {mpioco}_{\beta ,\gamma } \, N\) iff
The implemented management of a node hence conforms to its specification if, given a set of inputs, it can produce the expected outputs. In particular, if \(\beta \) is “\(\sqsupset \)” and \(\gamma \) is “\(=\)”, a candidate implementation conforms to a given specification only if it produces the same set of desired capabilities given exactly the same sets of requirements. This is, however, not the case in our running example, as the candidate implementation of api (hereafter denoted by \(\textsf {api} _I\)) can provide more outputs than those indicated by the specification (hereafter denoted by \(\textsf {api} _S\)). Indeed, by looking at the IOLTS encoding of the management protocol \(\textsf {api} _S\) (Fig. 4a) and at the input-enabled IOLTS encoding of that of \(\textsf {api} _I\) (Fig. 5), one can readily observe that \(\textsf {api} _I\) can output the capability endp in the configuration corresponding to the state installed, while \(\textsf {api} _S\) indicates that no capability is given as output in such configuration.
Setting \(\beta \) to “\(\sqsupset \)” and \(\gamma \) to “\(\ge \)” results in more flexible operators for management conformance testing. With \(\beta \) set to “\(\sqsupseteq \)”, conformance occurs also if the implementation can produce at least one of the expected sets of capabilities, hence enabling specifications to exhibit non-deterministic output behaviour. With \(\gamma \) set to “\(\ge \)” conformance occurs also if the implementation needs less requirements and provides more capabilities.
Relaxing \(\beta \) into “\(\sqsupseteq \)” is useless in our running example, as \(\textsf {api} _S\) is fully deterministic in its output behaviour. Relaxing \(\gamma \) into “\(\ge \)” is instead useful, as one can check that \(\textsf {api} _I \, \mathsf {mpioco}_{\sqsupset ,\ge } \, \textsf {api} _S \) and \(\textsf {api} _I \, \mathsf {mpioco}_{\sqsupseteq ,\ge } \, \textsf {api} _S\). One can indeed check that the IOLTS encoding of the management protocol \(\textsf {api} _S\) (Fig. 4a) and at the input-enabled IOLTS encoding of that of \(\textsf {api} _I\) (Fig. 5) are defined over the same input sequences, and that the latter can produce (at least) the same output sets as the former if given the same input sequences. However, which guarantees on the overall application management is given when choosing \(\textsf {api} _I\) to implement \(api_S\)? Is every possible trace of management preserved? Is there any (potentially undesired) additional trace that gets enabled?
Fig. 6
An alternative specification of the management protocol of api
×
Suppose now that we change the specification of the management protocol of api into that shown in Fig. 6, which we hereafter denote with \(\textsf {api} _S'\), for simplicity. \(\textsf {api} _S'\) gives more implementation freedom than \(\textsf {api} _S\), e.g., allowing the execution of the operation configure to exhibit different (non-deterministic) effects if invoked when api is installed. After deriving the IOLTS encoding of the management protocol of \(\textsf {api} _S'\) and testing the management conformance of \(\textsf {api} _I\) with \(\textsf {api} _S'\), one would obtain that \(\textsf {api} _I \, \mathsf {mpioco}_{\sqsupseteq ,=} \, \textsf {api} _S \) and \(\textsf {api} _I \, \mathsf {mpioco}_{\sqsupseteq ,\ge } \, \textsf {api} _S\) (while the same does not hold if \(\beta \) is set to “\(\sqsupset \)”). Which guarantees on the overall application management would be given when implementing \(\textsf {api} _S'\) by choosing \(\textsf {api} _I\)? Would such guarantees differ from those obtained when implementing \(\textsf {api} _S\) (instead of \(\textsf {api} _S'\)) with \(\textsf {api} _I\)?
5 Compositional testing
The different notions of \(\mathsf {mpioco}\) enable testing varying degrees of management conformance, which ensure different properties when choosing a conforming implementation to concretely implement a specified component. We now illustrate such compositionality properties (Section 5.1), and we discuss how they can drive the choice of which conformance tests to run (Section 5.2).
5.1 Compositionality properties
The overall management behaviour of an application A is defined by a labelled transition system defined over its global states [5], whose transitions are defined by two inference rules modelling operation execution and fault propagation (see Definition 3.4). To simplify the presentation of the compositionality properties resulting from testing management conformance, we hereafter denote such management behaviour as a composite application behaviour. The latter is a labelled transition system defined over a set of global states \({\mathcal {G}}_A\), whose initial state is the initial state for A, i.e., \({\overline{G}}_A\). Labels are then given by the operation or fault-handling transitions executed on the nodes in A (i.e., \(L_A=\bigcup _{N\in T}O_N\cup \{\bot \}\)), and the transition relation \(\rightarrow _A\) is the least relation satisfying the original inference rules in Definition 3.4.
Definition 5.1
(Composite Application Behaviour) Let \(A=\langle T,b\rangle \) be an application. Its composite application behaviour is defined by a labelled transition system \(\langle {\mathcal {G}}_A,{\overline{G}}_A,L_A,\rightarrow _A\rangle \) where
\({\mathcal {G}}_A\) is the set of global states of A,
\({\overline{G}}_A\) is the initial global state of A,
\(L_A=\bigcup _{N\in T}O_N\cup \{\bot \}\) is the set of transition labels, and
\({\rightarrow _A}\subseteq {\mathcal {G}}_A\times L_A\times {\mathcal {G}}_A\) is the least relation satisfying the rules op and fault in Def. 3.4.
The composite behaviour of an application defines its allowed management, which can also be characterised by the set of its composite traces. Intuitively, given the global state of an application, the composite traces for such state are given by the set of all sequences of operations and fault-handlers that can be executed from such global state. The set of all possible composite traces for an application are then given by the composite traces of its initial global state.
Definition 5.2
(Composite Traces) Let \(\langle {\mathcal {G}}_A,{\overline{G}}_A,L_A,\rightarrow _A\rangle \) be the composite application behaviour of application A. Let also G be a global state of A (i.e., \(G \in {\mathcal {G}}_A\)). \(\llbracket G \rrbracket \) denotes the set of composite traces for the global state G, which is the smallest set satisfying the following rules.
\(\epsilon \in \llbracket G\rrbracket \) and
if \(G\xrightarrow {\alpha }G'\) and \(\omega \in \llbracket G'\rrbracket \) then \(\alpha \omega \in \llbracket G\rrbracket \)
Notation 5.1
\(\llbracket A\rrbracket \) denotes all possible composite traces for an application A, with \(\llbracket A\rrbracket = \llbracket {\overline{G}}_A\rrbracket \).
Based on the composite traces defining the allowed management of an application, we can prove the compositionality properties resulting from the different operators for testing management conformance. The composite application behaviour obtained from management protocols adhere to a parallel step semantics including a synchronisation mechanism on shared requirements and capabilities. We hence frame the compositionality claims for \(\mathsf {mpioco}\) in terms of trace inclusion: consider two applications A and \(A'\), and suppose that \(A'\) is obtained by replacing the node N in A with \(N'\), with \(N' \mathsf {mpioco}_{\beta ,\gamma } N\).
(1)
If \(\mathsf {mpioco}\) holds with \(\beta \) set to “\(\sqsupset \)”, then \(A'\) preserves all the possible traces allowed by A, i.e., the composite traces for \(A'\) are at least those for A.
(2)
If \(\mathsf {mpioco}\) holds with \(\gamma \) set to “\(=\)”, then no additional trace is introduced in the allowed management of \(A'\), i.e., the composite traces for \(A'\) are at most those for A.
Theorem 5.1
(Compositionality Properties) Let \(A = \langle T, b \rangle \) be an application, and let \(N \in T\) be one of its nodes. Let also \(A' = \langle T', b \rangle \) be another multi-component application, with \(T' = (T - \{ N \}) \cup \{ N' \}\). If \(N' \mathsf {mpioco}_{\beta ,\gamma } N\), the following compositionality properties hold.
(1)
\(\llbracket A'\rrbracket \supseteq \llbracket A \rrbracket \Leftrightarrow \beta =\) “\(\sqsupset \)”, and
Let \(A = \langle T, b \rangle \) and \(A' = \langle T', b \rangle \) be multi-component applications. Suppose that \(A'\) is obtained from A by replacing its node N with \(N'\) (i.e., \(T'=(T-\{N\})\cup \{N'\}\)), with \(N'\,\mathsf {mpioco}_{\beta ,\gamma }\,N\). We hereafter prove properties (1) and (2) of Theorem 5.1 separately.
Table 1
Guarantees on overall application management, after implementing a specification by choosing a conforming implementation, with \(\mathsf {mpioco}\) varying on \(\beta \) and \(\gamma \)
\(\gamma \) is “\(=\)”
\(\gamma \) is“\(\ge \)”
\(\beta \) is “\(\sqsupset \)”
Existing traces preserved, no additional traces
Existing traces preserved
\(\beta \) is “\(\sqsupseteq \)”
No additional traces
—
(1)
We prove that \(\llbracket A'\rrbracket \supseteq \llbracket A \rrbracket \Leftrightarrow \beta \)=“\(\sqsupset \)”. By Notation 4.3, it holds that \(Z'\sqsupseteq Z''\) iff \(\forall z'\in Z':(\exists z''\in Z'':z''\subseteq z')\). It hence follows that \(\forall \sigma \in \mathsf {straces}({\overline{s}}_{N})\,.\,\mathsf {out}(\mathsf {reach}_{\gamma }({\overline{s}}_{N'},\sigma ))\,\sqsupseteq \,\mathsf {out}(\mathsf {reach}_{\gamma }({\overline{s}}_{N},\sigma ))\) (see Def. 4.8), which means that the capabilities of \(N'\) must be at least those provided by N in every state. Furthermore, we may remove requirements (case \(\gamma \in \{\ge \}\)) or leave requirements unchanged (case \(\gamma \in \{=,\ge \}\)) in \(N'\) as compared to N. As a result, no required capabilities may be dropped and no requirements may be added, such that \(\forall \sigma \in \llbracket A\rrbracket :\sigma \in \llbracket A'\rrbracket \). Additionally, \(\beta \)=“\(\sqsupset \)” does not affect fault handling as requirements can only be dropped (as explained above). Therefore, \(\llbracket A'\rrbracket \supseteq \llbracket A\rrbracket \Leftrightarrow \beta \)=“\(\sqsupset \)”.
(2)
We prove that \(\llbracket A'\rrbracket \subseteq \llbracket A\rrbracket \Leftrightarrow \gamma \)=“\(=\)”. By definition, \(x\in \mathsf {reach}_{=}(N',\sigma )\) with \(\sigma \in \textit{straces}(N)\) iff the following recursive rules hold (see Def. 4.7):
\(x \in \mathsf {reach}_{=}(x',\sigma )\) if \(x' \xrightarrow {C'}_N x'' \wedge C' \subseteq C_N \wedge \sigma = C' \cdot \sigma '' \wedge x \in \mathsf {reach}_{=}(x'',\sigma '')\),
\(x \in \mathsf {reach}_{=}(x',\sigma )\) if \(x' \xrightarrow {\textit{o}^\uparrow } x'' \wedge o \in O_N \wedge \sigma = \textit{o}^\uparrow \cdot \sigma '' \wedge x \in \mathsf {reach}_{=}(x'',\sigma '')\), and
\(x \in \mathsf {reach}_{=}(x',\sigma )\) if \(x' \xrightarrow {\textit{o}^\downarrow } x'' \wedge o \in O_N \wedge \sigma = \textit{o}^\downarrow \cdot \sigma '' \wedge x \in \mathsf {reach}_{=}(x'',\sigma '')\).
Hence, \(x\in \mathsf {reach}_{=}(N',\sigma )\) iff there exists a trace to x in N consisting of the same inputs and outputs (i.e., requirements and capabilities) as trace \(\sigma \) of N. Furthermore,
This means that \(N'\) may have the same outputs as N (case \(\beta \in \{\sqsupseteq \}\)), or that N only implements some of the possible outputs of \(N'\) (case \(\beta \in \{\sqsupseteq \),\(\sqsupset \}\)). It may hence be that \(\exists \sigma ''\in \llbracket A\rrbracket :\sigma ''\notin \llbracket A'\rrbracket \) as capabilities (i.e., outputs) of N required by other nodes may be dropped. However, by Def. 4.7 no requirements may be dropped and no additional capabilities may be added in \(N'\) as otherwise \(N'\,\mathsf {mpioco}_{\beta ,=}\,N\) would not hold. This results in \(\llbracket A\rrbracket \not \subset \llbracket A'\rrbracket \). Additionally, \(\gamma \)=“\(=\)” does not affect fault handling as no requirements can be dropped (as explained above). Therefore, \(\llbracket A'\rrbracket \subseteq \llbracket A\rrbracket \Leftrightarrow \gamma =\) “\(=\)”.\(\square \)
5.2 Which Conformance Testing Operator to Exploit?
The different operators that can be obtained from \(\mathsf {mpioco}\) ensure also different compositionality properties when implementing a component specification by choosing a conforming, available implementation (Theorem 5.1). Stricter constraints on the parameters \(\gamma \) and \(\beta \) of \(\mathsf {mpioco}\) (i.e., setting \(\gamma \) to “\(=\)” or \(\beta \) to “\(\sqsupset \)”) result in stricter operators for testing management conformance, which induce additional guarantees on the overall management behaviour of a multi-component application (Table 1).
Whenever a candidate implementation for a component conforms to its specification with \(\beta \) set to “\(\sqsupset \)”, implementing the specification by choosing the conforming implementation results in preserving all possible traces in the overall management behaviour of an application. Conversely, no additional trace is introduced when implementing the specification of a component by choosing an implementation that conforms to such specification with \(\gamma \) set to “\(=\)”.
Notably, the choice of which restrictions on \(\beta \) or \(\gamma \) to employ (and hence which testing operators to employ) strictly depends on the guarantees that an application administrator wishes to have. If an application administrator wishes to implement the specification of a component by preserving the overall management behaviour of the application it appears in, she must test the management conformance of a candidate implementation with \(\beta \) set to “\(\sqsupset \)”. The latter was precisely the case in our running example (Section 2), where we wished to ensure that the already developed management plans will continue to work properly after implementing the specification \(\textsf {api} _S\) (Fig. 3a) by choosing \(\textsf {api} _I\) (Fig. 3b). Given that \(\textsf {api} _I\) shown to be conforming to \(\textsf {api} _S\) with \(\beta \) and \(\gamma \) set to \(\sqsupset \) and \(\ge \) (Section 4.3), we can exploit \(\textsf {api} _I\) to implement \(\textsf {api} _S\) while at the same time being sure that the formerly allowed management behaviour is preserved, hence meaning that plans devised for managing the application will continue to work.
Alternatively, if an application administrator wishes to implement the specification of a component by ensuring that no additional management trace is introduced, she has to test for management conformance with \(\gamma \) set to “\(=\)”. This property is not to be underestimated, as enabling additional management activities while considering interdependent components may result in some undesired situation. For instance, a component specification may require the use of a VPN in some states to secure its communications. With the relaxed version of \(\gamma \), an implementation never requiring any VPN would conform the specification, even if it this would mean that choosing such implementation would result in not exploiting any VPN to secure communications. For avoiding such a kind of undesired situations to happen, \(\mathsf {mpioco}\) is hence to be tested by setting \(\gamma \) to “\(=\)”, which disallows additional management activities to get enabled in applications where the specification of a component has been implemented by choosing a conforming implementation.
Consider again, for instance, the alternative specification for the management of \(\textsf {api} \), i.e., \(\textsf {api} _S'\) (Fig. 6). The latter allows some implementation freedom, e.g., by allowing to freely choose how to implement the operation configure that can be invoked in state installed. Suppose now that the application administrator wishes to implement such specification with the candidate implementation \(\textsf {api} _I\) shown in Fig. 3b, while at the same time ensuring that no additional management activity gets enabled. She should then test the management conformance of \(\textsf {api} _I\) with respect to \(\textsf {api} _S'\) with \(\gamma \) set to “\(=\)”, which can be shown to hold (see Section 4.3). It hence means that the \(\textsf {api} _I\) can be chosen to implement \(\textsf {api} _S'\), while at the same time being sure that (at most) only the management activities that were allowed by the specification \(\textsf {api} _S'\) will continue to be allowed after choosing \(\textsf {api} _I\) used to implement it.
6 Prototype and experiments
We now present a prototype implementation of the proposed approach (Section 6.1) and the results of its application to controlled experiments (Section 6.2). The sources of the prototype and experiments are available on GitHub.5
6.1 Prototype
Our prototype automatically checks whether \(N' \, \mathsf {mpioco}\, N\) holds between a candidate implementation \(N'\) and a corresponding specification N both explicitly given as compositions of management protocols. Our prototype accepts as input a predefined XML file format containing the descriptions of the management protocols of the desired component N and of the available implementation \(N'\).6 In addition, it allows setting the values of the parameters \(\beta \) and \(\gamma \) to control the configuration of the \(\mathsf {mpioco}\) relation.
In the following, we briefly sketch the different steps performed by the prototype to verify whether \(N' \ \mathsf {mpioco}\ N\) holds.
1.
IOLTS transformation: After parsing the input files, the management protocol models N and \(N'\) are transformed into IOLTS models to serve as a basis for checking \(\mathsf {mpioco}\) as described in Sect. 4.
2.
Input completion: The IOLTS encodings of the input models are checked for input-enabledness, and input-completion is applied where necessary.
3.
Conformance checking: To check whether \(N' \, \mathsf {mpioco}\, N\) holds, the prototype runs the procedures for the functions out and reach as well as for the derivation of the set of straces from the specification.
To evaluate the potential gains in efficiency of compositional checking of \(\mathsf {mpioco}\), our prototype is further able to handle input models consisting of networks of multiple nodes by constructing the respective composite application before applying the \(\mathsf {mpioco}\) check as described in Section 5.
6.2 Experimental Evaluation
We considered the following research questions:
(RQ1)
What is the computational effort of the \(\mathsf {mpioco}\)-check depending on the number of suspension traces?
(RQ2)
What is the potential gain in efficiency of compositional \(\mathsf {mpioco}\)-checking as compared to checking composite applications?
Experimental Set-up. To answer to RQ1 and RQ2, we created five different subjects systems based on the socc_Docker application publicly available at the GitHub repository of management protocol’s reference implementation [5].7 In particular, to systematically investigate the impact of the number of nodes for answering RQ2, we considered five different versions of socc_Docker, referred to as sDk, where k denotes the number of nodes (see first row of Table 2).
Table 2
Results of our experimental evaluation
sD1
sD2(a)
sD2(b)
sD3
sD4
# nodes
1
2
2
3
4
# states (com)
11
72
152
400
2048
# states (nbn)
11
22
28
33
44
# straces (com)
32
21,138
264,533
>1,000,000
n/a
# straces (nbn)
32
64
82
96
128
CPU time (com)
0.13s
1.20s
6,77s
>1h
n/a
CPU time (nbn)
0.13s
0.02s
0.02s
0.04s
0.05s
To investigate the performance measures of \(\mathsf {mpioco}\)-checks \(N' \, \mathsf {mpioco}\, N\), we require for each experimental run two input models, i.e., a specification N and an implementation under test \(N'\). Our prototype consecutively derives further suspension traces from specification N as long as the corresponding output of the implementation \(N'\) for these suspension traces conforms to those permitted by specification N. Once a non-conforming suspension trace is observed, the check terminates, reports that \(N' \mathsf {mpioco}N\) does not hold and returns the failed trace as a witness. Concerning the computational effort for a complete run of the \(\mathsf {mpioco}\)-check, the worst case arises whenever \(N' \, \mathsf {mpioco}\, N\) actually holds as this requires the derivation of all (loop-free) suspension traces from N. Hence, we performed each experimental run as \(N \, \mathsf {mpioco}\, N\) to gain worst-case run-time measures.
To answer RQ2, we considered two checks:
Composite check (com): Given a pair of implementation/specification both consisting of k nodes, we first construct one IOLTS representing the composite management application by applying the parallel-composition operator on the corresponding IOLTS representations of the respective nodes [13]. We then perform one \(\mathsf {mpioco}\)-check between the IOLTS of the composite applications.
Node-by-node check (nbn): Given a pair of implementation/specification both consisting of k nodes, we perform k\(\mathsf {mpioco}\)-checks, one for each pair of nodes in separate utilising the compositionality property of \(\mathsf {mpioco}\).
Table 2 contains the number of states of the IOLTS for both kinds of checks per subject system. In case of (com), the number of states is roughly given as \(|S|^k\), where |S| is the (average) number states of the IOLTS of one node. In case of (nbn), the number of states is given as the sum of states of the IOLTS of the k nodes.
For answering (RQ1), we counted the overall number of suspension traces generated from the IOLTS of the specification and measured the overall CPU time required for the \(\mathsf {mpioco}\)-checks by testing those sets of traces on the implementation. In addition, for answering (RQ2), we compare both measures obtained for (com) with those obtained for (nbn).
Results and discussion. The measurement results in Table 2 for (com) indicate a fast exponential increase of both the number of suspension traces as well as the required CPU time with an increasing number k of nodes. For \(k=3\), the CPU time already exceeds 1h and for \(k=4\), the \(\mathsf {mpioco}\)-check does not terminate within a reasonable amount of time. In contrast, in case of (nbn), we observe a linear increase of the number of suspension traces and the required CPU time with an increasing number k of nodes, where both values remain negligibly small even in case of \(k=4\).
The experimental results hence show that the compositionality properties make \(\mathsf {mpioco}\)-check practically applicable to composite applications, already in case of a very small number of nodes.
7 Related work
We now position our contribution with respect to the state of the art by first discussing design-time approaches for safely choosing the implementation of application components in multi-component applications. We then position our proposed I/O conformance testing approach with respect to other existing solutions for conformance testing.
Implementing specified components. To the best of our knowledge, [10] and [14] are the only existing solutions for finding suitable implementations of specified application components by considering how candidate implementations can be managed, with [10] checking management congruence by means of ontologies. [14] is a step closer to our framework, since it also considers the interaction of chosen implementations with the other components of an application when coordinating their overall management, by still exploiting topology graphs and management protocols to specify the structure and management behaviour of multi-component applications. It, however, assumes the management protocols of candidate implementations to be always known, to then apply simulation and co-induction to check whether they can be chosen to implement a component specification. We instead enable choosing also candidate implementations given as black-boxes, thanks to I/O conformance testing [7].
Other approaches worth mentioning are those choosing among candidate implementations of specified components based on their functionalities. For instance, [15] exploits Petri nets to assess behaviour-preserving choice of web services, while [16] and [17] propose two different solutions for the behaviour-preserving matching of web services. We actually complements such approaches, since we consider the allowed management of candidate implementations, rather than their functionalities. In addition, all such approaches (as well as [10] and [14]) consider an implementation as suitable to implement the specification of a component if the implementation can provide (at least) the desired outputs if provided with (at most) the same inputs, by also providing techniques for adapting matching implementations to exhibit the specified I/O behaviour. Their goal is indeed to implement a component specification by choosing a suitable implementation, and by ensuring that the overall application behaviour is preserved, which in our case can be obtained by exploiting \(\mathsf {mpioco}\) with \(\beta \) restricted to “\(\sqsupset \)”. Our approach instead supports application administrators in a wider set of scenarios, which vary on the guarantees they wish to get on the overall management of an application.
Similar considerations apply to the solution proposed in [18], which checks whether the interactions with a component in a multi-component application conforms to the behaviour specified by the component itself, including its exception handling. The ultimate goal of [18] is indeed to preserve the overall application behaviour. Our approach is intended to be applicable to a wider set of scenarios, differentiated by the guarantees on the overall application management that an application administrator wishes to have.
Conformance testing. Various solutions have been proposed to check the conformance of an available implementation to a given specification. For instance, [19] proposes a context-aware declarative reasoning for conformance checking. [20] proposes a randomised testing solution for checking conformance of systems whose internals are unknown. [21] allows to test the conformance of a software process by proposing a methodology to elicit possible violations. The main difference between the above solutions and ours resides in the objectives and applied method, as we build upon Tretmans’ I/O conformance theory [7] to test management conformance. We chose I/O conformance testing to explicitly deal with the I/O behaviour defined by management protocols, while still fitting to black-box scenarios [7], supporting compositionality [12], and enabling implementation freedom [22].
We hence position our framework with respect to other existing extensions of Tretmans’ I/O conformance testing. The closest to ours are those (i) considering implementation freedom due to specifications with non-deterministic output behaviour, (ii) explicitly modelling fault handling, and (iii) providing guarantees on the overall application behaviour after implementing a specification by choosing a conforming implementation.
As for (i) implementation freedom, approaches worth mentioning are [23‐27]. [23] extends I/O conformance testing to support implementation freedom in software product lines, with behavioural variability controlled by feature selection. [24] and [25] introduce modality in I/O conformance testing, which enables distinguishing mandatory output behaviour from optional output behaviour. Modality is used to enable implementation freedom also in [26] and [27], which lift conformance from trace inclusion to preorders defined by means of alternating simulation relations [28]. At the same time, none of such approaches captures the implementation freedom characterising our proposed management conformance testing, e.g., allowing an implementation to need less requirements or provide more capabilities than the specification.
As for (ii) fault-handling, to the best of our knowledge, our framework is the first for I/O conformance testing in multi-component applications that explicitly models fault-handling. The only other approaches explicitly including faults are those in [12, 22], even if for different purposes. They indeed model explicit fault states, which constitute forbidden states used to suspend conformance testing runs to handle the case of forbidden inputs. However, [12, 22] does not support the explicit specification and testing of fault-handling mechanisms such as those natively provided by management protocols.
Finally, our framework differs from the state of the art in I/O conformance testing along the (iii) compositionality dimension. Most of the compositionality results obtained for I/O conformance testing are formulated in the flavour first proposed in [13], i.e., by composing the I/O behaviour of application components with some cross-product-style operator emulating parallelism at the level of the IOLTS encoding their semantics. Concrete examples in this direction are [12, 22, 29‐33]. However, the composition of management protocols [5] is not based on any cross-product-style operator, but rather on inference rules dealing with the interplay among requirements and capabilities. Our proposal for testing management conformance hence not only differs in supported tests, but also in the accompanying compositionality results, which have to consider a different composition approach.
Summary. To the best of our knowledge, ours is the first approach for testing conformance of the management allowed by a candidate implementation for a component with respect to that of its specification. Our approach differs from existing solutions for the behaviour-aware choice of candidate implementations in terms of supported scenarios, enabled by the proposed parametric relation of conformance testing. The latter is the first relation providing the freedom to implement a specification by “requiring less” and “offering more”, dealing with explicit fault-handling, and with inference rules to derive the behaviour of application components.
8 Conclusions
We have introduced a framework enabling to test management conformance in multi-component applications. More precisely, we have proposed a parametric relation that enables testing whether the management allowed by a candidate implementation for a component conforms to its specification, with the latter given in terms of management protocols [5]. Our parametric relation can be instantiated into four different conformance testing operators, which provide different guarantees on the overall application management after implementing a component specification by choosing a conforming implementation.
Which operator to exploit depends on the desiderata of an application administrator and on her testing capabilities. Stricter testing operators reduce the number of conforming implementations and require more configuration efforts, but they enable fully preserving already allowed application management when choosing a conforming implementation to implement a specified component, and/or ensuring that no novel management activity gets allowed. Preserving application management enables to continue using already devised plans for managing an application, as it ensures that such plans would continue to work. Ensuring that no novel management activity gets enabled is instead fundamental to avoid that unintended interactions get enabled, as this could cause possibly undesired situations for the application, e.g., with components that start communicating even if no secure channel has been established yet.
We have also assessed the applicability of the proposed management conformance testing and of its compositionality properties by means of a prototype and an experimental evaluation. In doing so, we have worked in a white-box setting, with the tester having knowledge also on the implementations’ the behaviour of operations, requirements, and capabilities during testing. This was just for simplicity, and without loss of generality: to work in a black-box setting, it is enough to equip the (unknown) implementation under test with a monitoring interface that makes operations, requirements, and capabilities observable during testing. The development of a monitoring support to enable observability of operations, requirements, and capabilities on available implementations is in the scope of our future work.
For future work, we also plan to extend the set of supported management conformance tests, with three concrete actions already pinned in our research roadmap. We plan to adapt our management conformance checking to consider the possibility of replicating a component, based on the recently released replica-aware management protocols [34]. We also plan to include modality to further extend the degree of implementation freedom, similarly to what done in [24] and [25] for other types of I/O conformance testing. Finally, we plan to expand the set of supported means for specifying the management of multi-component applications by adapting our solution to work with other approaches for modelling application management, e.g., the Aeolus component model [1].
Declarations
Conflict of interest
The authors also do not have any conflict of interests relevant to content presented in this article. The authors have no relevant financial or non-financial interests to disclose, nor competing interests to declare that are relevant to the content of this article.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
The set of management operations available to the orchestrator is the union of the sets of management operations available on each of the components of an application.
Fault handlers enable modelling that the fault of a requirement results in the application getting to a partly working state from which it can be recovered, as well as that such fault is unforeseen and results in a sudden “crash” of the application. Further details and examples can be found in [5].
For simplicity, and without loss of generality, we assume that the names of states, requirements, capabilities, and operations of the nodes in a topology are all disjoint.
We assumed a white-box setting in our experiments, with the protocol of available implementations given as input, rather than being observed by equipping the implementation under test with a monitoring interface that makes operations, requirements, and capabilities observable during testing. The white-box setting is hence only assumed to simplify the set-up of our experiments, but without threatening their validity.
, and