       
@ 2013 - Site Map - Credits |
 |
Dynamic CONNECTor Synthesis |
| |
|
| Objectives |
Our work on dynamic CONNECTor synthesis aims at devising associated automated and compositional approaches, which can be performed at run-time. Starting from (i) the respective interaction behaviour of networked systems modelled as LTSs, and (ii) their ontology-based interface specifications, we want to synthesize the CONNECTors that are needed for networked systems to interoperate. These CONNECTors mediate the interaction between the networked systems at both application- and middleware-layers.
|
| |
Our objectives subdivide into:
- Synthesis of application-layer conversation protocols: the goal here is to identify CONNECTor patterns that allow the definition of methodologies to automatically synthesize, in a compositional way and at run-time, application-layer CONNECTors.
- Synthesis of middleware-layer protocols: our objective here is to generate adequate protocol translators (mappings) that enable heterogeneous middleware to interoperate, and realize required non-functional properties, thus successfully interCONNECTing networked systems at the middleware level.
- Model-driven synthesis tools: we exploit model-to-model and model-to-code transformation techniques to automatically derive, at run-time, a concrete CONNECTor from its synthesized model. The concrete CONNECTor may then be deployed in the environment, thereby enabling networked systems to interoperate. This step should guarantee the correctness-by-construction of the CONNECTor’s implementation with respect to the functional and non-functional requirements of the networked applications that are made interoperable through the CONNECTor.
Overview of the Automated CONNECTor Synthesis Approach
The figure below outlines our overall approach to support the dynamic synthesis of CONNECTors given Networked Systems (NSs) models and the ontologies describing the domain-specific knowledge.
|
The Synthesis of an Abstract CONNECTor (i.e., CONNECTor model) is preceded by two steps:
- Functional Matching consists of checking whether, at a high level of abstraction, the functionality (referred to as affordance) required by one system can be provided by the other. This is realized by checking the semantic compatibility of the NSs affordances using ontology reasoning.
- Middleware Abstraction makes the behaviour of NSs middleware-agnostic , i.e., it abstracts/translates (sequences of) middleware functions into input/output application actions in order to focus on the application-specific semantics.
Subsequently, the Abstract CONNECTor Synthesis process is made up of three steps:
- Identification of the Common Language makes comparable the NSs behaviour by identifying their common language and, possibly, reduces their size thus allowing to ease and speed up the reasoning on them.
- Behavioural Matching checks the NSs compatibility from a functional perspective while identifying possible behavioural mismatches.
- Mediator Synthesis produces a mediator that overcomes the identified behavioural mismatches between the two NSs so as to allow them to interoperate.
Once the Abstract CONNECTor is synthesised, it is concretized by making the CONNECTor model middleware-aware, thereby enabling to generate appropriate middleware messages on the wire. The concrete CONNECTor is ultimately deployed in the network, further running on top of the CONNECTor engine (i.e., StarLink developed as part of the CONNECT architectural framework) for the actual synthesis of middleware messages on-the-fly. |
| Overview of the Abstract CONNECTor Synthesis Enabler |
The figure below outlines the architecture of the Synthesis Enabler. It provides the synthesiseAbstractMediator method that is called by the Discovery Enabler to initiate the synthesis process after finding a functionally compatible pair of NSs. |
 |
The Synthesis Enabler takes as input the models of two NSs to be CONNECTed and generates the model of a CONNECTTor that allows them to interoperate. The Enabler then verifies that the CONNECTor model meets the non-functional requirements of the interaction between the two NSs by calling the Analyze method provided by the CONNECTability Enabler. Finally, the Synthesis Enabler sends the synthesized model to the Deployment enabler so that it is executed on top of the StarLink framework.
While the Synthesis Enabler displays a unique interface, there are two approaches to the synthesis of mediators that are implemented: goal-based and mapping-driven synthesis. In a nutshell:
- Goal-based synthesis tries to synthesize a CONNECTor solving a reachability problem between the interfaces (alphabets) of two networked systems. In a first phase, this approach tries to determine a common language, reasoning on a domain-specific ontology. Then it tries to find a possible run on the parallel product of the two NSs protocols that satisfies some progress and consistency properties ensuring that the two NSs can communicate, and such that the run satisfies a user goal, provided as input to the approach. This is formulated as a reachability problem and is solved using a model checker. The model checker gives as output only one of the possible traces satisfying the goal, therefore this process is repeated until all the feasible interactions are found (or until an upper bound on the trace length is reached, in case of protocols featuring loops).
- Mapping-driven synthesis first focuses on the interfaces of both NSs and combines ontology reasoning and constraint programming to identify the semantic correspondence between the networked systems’ interfaces, i.e., interface mapping. The interface mapping specifically defines the correspondence between the actions of the systems’ interfaces so as to generate the mapping processes that perform the necessary translations between actions. Unlike existing approaches to interface mapping that only tackle the one-to-one correspondence between actions, this approach handles the more general cases of one-to-many and many-to-many mappings. Furthermore, the ontology is encoded so as to make the reasoning more efficient at runtime. We use an ontology-based model checking technique to explore the various possible mappings in order to produce a correct-by-construction mediator that guarantees that the two systems can successfully interact. More specifically, we generate the parallel composition of the mapping processes and verify that the overall system successfully terminates using the LTSA (Labelled Transition System Analyser) model checker. Furthermore, we are improving the algorithm so as to deal with ambiguous mappings, i.e., when an action from one system may semantically be mapped to different actions from the other system. The synthesised mediator model ensures the safe interaction between the NSs, i.e., it ensures deadlock-freeness and the absence of unspecified receptions (since we assume blocking sends), whatever goal is considered.
The Synthesis Selector chooses the most appropriate synthesis approach among the above two. Currently, this is based on whether a goal is provided as input or not to the Synthesis Enabler. The two approaches relies on the same modules for middleware abstraction and for transforming the mediator model into a k-coloured automata, that is a concrete model of the mediator that can be interpreted by the CONNECTor engine (i.e., StarLink). |
| |
Selected Publications
|
| Further Information |
| More information about the work on dynamic CONNECTor synthesis can be found from the Publications page. |
|
