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.

Info-Icon Diese Seite ist nicht in Deutsch verfügbar
Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Bildinformationen anzeigen

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

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.

Participant: Arnab Sharma

Former Participants: Galina Besova, Sven Walther, Julia Krämer

Cooperation (nonfunctional analysis): RG Hüllermeíer

Former Cooperation (nonfunctional analysis):
 Prof. Dr. Steffen Becker

Official website.


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, 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 also must be done with 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 composition. But such techniques are time consuming and difficult to apply in on-the-fly composition. The central approach of this project 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 fault 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, this encompasses balanced usage of training data. 


This project is funded by the Deutsche Forschungsgemeinschaft DFG (Collaborative Research Center 901)


Prof. Dr. Heike Wehrheim

Spezifikation und Modellierung von Softwaresystemen

Heike Wehrheim
+49 5251 60-4331

Arnab Sharma

Spezifikation und Modellierung von Softwaresystemen

Arnab Sharma
+49 5251 60-5388
+49 5251 60-3993

Die Universität der Informationsgesellschaft