Verifying deadlock- and livelock freedom in an SOA scenario

K. Wolf, C. Stahl, J. Ott, R. Danitz

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)


In a service-oriented architecture (SOA), a service broker assigns a previously published service (stored in a service registry) to a service requester. It is desirable for the composition of the requesting and the assigned service to interact properly. While proper interaction is often reduced to deadlock freedom of the composed system, we additionally consider livelock freedom as a desirable property for the interaction of services. In principle, deadlock- and livelock freedom can be verified by inspecting the state space of the composition of (public views of) the involved services. The contribution of this paper is to propose a methodology to build that state space from pre-computed fragments which are computed upon publishing a service. That way, we shift computation time from the time critical "request" phase of service brokerage to the less critical "publish" phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions.
Original languageEnglish
Title of host publicationProceedings 9th International Conference on Application of Concurrency to System Design (ACSD 2009, Augsburg, Germany, July 1-3, 2009)
PublisherInstitute of Electrical and Electronics Engineers
ISBN (Print)978-0-7695-3697-2
Publication statusPublished - 2009


Dive into the research topics of 'Verifying deadlock- and livelock freedom in an SOA scenario'. Together they form a unique fingerprint.

Cite this