Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

CRC 901 – On-The-Fly Computing (OTF Computing) Show image information

CRC 901 – On-The-Fly Computing (OTF Computing)

Service Composition Analysis in Partially Unknown Contexts

Subproject B3 of CRC 901

Subproject B3 researches analysis methods for service compositions that evaluate the fulfilments of functional and non-functional requirements. In this, functional requirements might be described by logical pre- and postconditions or protocol specifications; non-functional requirements might concern the runtime or memory consumption, but also the reputation of an assembled composition.

Functional Requirements

Fig. 1: Concept of template based verification to check the correctness of service compositions

Software quality is an important matter in many application areas of modern software engineering. A key to achieve it is the usage of formal analysis. Formal stands for the specification of software using formal models and the analysis of these models using formal methods with respect to certain properties.

In case of service oriented architectures where different services are composed together, those are often need to be assembled or changed on-the-fly. This creates huge challenges to guarantee the desired quality of such composed services. Here ‘quality’ refers to both the functional and non-functional requirements. Analysis of such services must be done within a specified time thereby imposing timing constraints. Different quality assurance method works by transforming a composition into an analysis model which captures the semantics of the service composition. But such techniques are time consuming and difficult to apply in on-the-fly compositional process. The main idea of our work is to use templates which capture the known compositional patterns and verify those using Hoare-style proof calculus to prove their correctness.

Fig. 1 illustrates our approach. Templates are defined as workflow descriptions with service placeholders, which are replaced by concrete services during instantiation. Every template specification contains pre- and post-conditions which are used to verify the correctness of the templates. Once a template has been proven correct, we only need to prove certain side conditions for the instantiations and can then conclude their correctness.

Fig. 2: Localizing faults in service composition

Our work also encompasses localizing the faults in such service compositions. The intention of fault localization is to identify the services most likely causing the fault ( see Fig. 2). To this end, we use a logical encoding of the service composition and it's requirement, and apply a maximum satisfiability solver on it to locate faults. 

Ongoing work

As the CRC 901 currently investigates on-the-fly assembled Machine Learning (ML) applications, subproject B3 has started to investigate specific analysis questions for ML services. On the functional side, one such property encompasses balanced usage of training data. 

Non-Functional Requirements

In general, we can distinguish between two different non-functional property classes: external quality properties and internal quality properties. External quality properties, like performance, reliability, or scalability, directly influence the user experience. Internal quality properties, like maintainability and reusability, may only have indirect influence on the user experience. Our focus in subproject B3 is on the analysis of external quality properties, e.g. performance, of services composed on-the-fly upon user request.

Figure 1: Simulation-based analysis of service compositions. The inputs for the analysis are a service specification with its usage context, optionally adaptations, and the service level objectives. The output are values for performance and elasticity metrics.

We predict the performance of a service composition and check whether its service level agreements will hold. To this end, we transform knowledge about the composition into analysis models, e.g. queuing networks, which we can analyze. For this analysis context of the composition, like the available hardware resources at run-time and the frequency service calls, is required. However, this context information may not be complete or not available at all.

Figure 1 illustrates our approach. We are developing an engineering method that supports service providers to model resource-efficient and elastic self-adaptive multi-resource systems. The method also helps in identifying and deciding quality trade-offs. Multiple relevant quality metrics can be predicted such that design deficiencies in the software architecture and self-adaptation capabilities that limit resource-efficiency and elasticity can be identified. These results are then fed back into the matching, developed in Subproject B1.

For the analysis we reuse the software performance engineering tool Palladio, which is actively developed at the University of PaderbornTechnische Universität ChemnitzKarlsruhe Institute of Technology (KIT), and FZI Research Center for Information Technology

Model Transformations

The sub-project B3 of the CRC "On-The-Fly Computing" is concerned with the model-based analysis of functional and non-functional properties of service compositions created by sub-project B2. Since different formalisms like layered queueing networks and process algebras are used to analyze these properties, B3 has to develop multiple complex transformations of service composition models into these formalisms.

To address this issue, we have proposed a model transformation development approach, which allows simplifying and improving the quality of the developed transformations via the exploitation of the languages’ structures. The approach is based on context-free graph grammars, used for the definition of modeling languages, and transformations, defined by pairing productions of these source and target grammars in a certain way. We have shown that model transformations defined using this approach and conforming to its requirements, exhibit three important characteristics: they are sound, complete, and deterministic.

To be able to re-use the developed quality model transformation in the cases where service compositions are modeled at different levels of abstraction (e.g., with or without platform/infrastructure services models), we have proposed a modular approach based on weaving models. This approach allows modeling of inter-service interactions in a non-invasive way, as weavings. Furthermore, by subjecting weaving models to a separate model transformation, it enables re-use of existing model transformations for the individual woven models.

Further Information

For further information about, please consult our publications or contact our researchers.

The University for the Information Society