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.

Participants: Heike Wehrheim, Arnab Sharma

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

Cooperation (non-functional analysis): RG Hüllermeíer

Former Cooperation (non-functional analysis): Prof. Dr. Steffen Becker

Official website.

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.

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. 

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)

Publications of SFB 901 B3