Spreading excellence and disseminating the cutting edge results of our research and development efforts is crucial to our institute. Check for our educational offers for Bachelor, Master and PhD studies at the University of Innsbruck!

Service Composition and Automated Theorem Proving: A Survey on Existing Approaches

Student name: 

Semantic annotation of services or components can help to locate those ones, which provide a specific functionality that is requested by some client. This question is one aspect of a process called service discovery which can help in the dynamic and (semi)automated construction of software systems. In open environments and large component marketplaces, the assumption to find a single entity which is capable of providing precisely the required functionality breaks down in general: for more sophisticated problems one will not be able to find a single adequate service. On the other hand in not too specific cases, there is still hope to find a combination of several available services which as a whole satisfies the given requirements. The process of finding resp. developing such a combination of services is called service composition. In particular there has been some work on automating (parts of) a composition by using automated theorem proving techniques. The purpose of this thesis is to look at those approaches, summarize and compare them and perhaps do some experiments with existing tools.