Knowledge-Based Verification of Service Compositions - An SMT approach

S. Walther, H. Wehrheim, in: Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32.

Download
Restricted 06601801.pdf 217.09 KB
Conference Paper | English
Author
Walther, Sven; Wehrheim, HeikeLibreCat
Abstract
In the Semantic (Web) Services area, services are considered black boxes with a semantic description of their interfaces as to allow for precise service selection and configuration. The semantic description is usually grounded on domain-specific concepts as modeled in ontologies. This accounts for types used in service signatures, but also predicates occurring in preconditions and effects of services. Ontologies, in particular those enhanced with rules, capture the knowledge of domain experts on properties of and relations between domain concepts. In this paper, we present a verification technique for service compositions which makes use of this domain knowledge. We consider a service composition to be an assembly of services of which we just know signatures, preconditions, and effects. We aim at proving that a composition satisfies a (user-defined) requirement, specified in terms of guaranteed preconditions and required postconditions. As an underlying verification engine we use an SMT solver. To take advantage of the domain knowledge (and often, to enable verification at all), the knowledge is fed into the solver in the form of sorts, uninterpreted functions and in particular assertions as to enhance the solver’s reasoning capabilities. Thereby, we allow for deductions within a domain previously unknown to the solver. We exemplify our technique on a case study from the area of water network optimization software.
Publishing Year
Proceedings Title
Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)
Page
24 - 32
LibreCat-ID
517

Cite this

Walther S, Wehrheim H. Knowledge-Based Verification of Service Compositions - An SMT approach. In: Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS). ; 2013:24-32. doi:10.1109/ICECCS.2013.14
Walther, S., & Wehrheim, H. (2013). Knowledge-Based Verification of Service Compositions - An SMT approach. In Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) (pp. 24–32). https://doi.org/10.1109/ICECCS.2013.14
@inproceedings{Walther_Wehrheim_2013, title={Knowledge-Based Verification of Service Compositions - An SMT approach}, DOI={10.1109/ICECCS.2013.14}, booktitle={Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)}, author={Walther, Sven and Wehrheim, Heike}, year={2013}, pages={24–32} }
Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service Compositions - An SMT Approach.” In Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 24–32, 2013. https://doi.org/10.1109/ICECCS.2013.14.
S. Walther and H. Wehrheim, “Knowledge-Based Verification of Service Compositions - An SMT approach,” in Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32.
Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service Compositions - An SMT Approach.” Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32, doi:10.1109/ICECCS.2013.14.
Main File(s)
File Name
06601801.pdf 217.09 KB
Access Level
Restricted Closed Access
Last Uploaded
2018-11-02T13:26:08Z


Export

Marked Publications

Open Data LibreCat

Search this title in

Google Scholar