  The assurance of quality of service properties is an important aspect of
service-oriented software engineering. Notations for so-called service level
agreements (SLAs), such as the Web Service Level Agreement (WSLA) language,
provide a formal syntax to specify such assurances in terms of (legally
binding) contracts between a service provider and a customer. On the other
hand, formal methods for verification of probabilistic real-time behavior have
reached a level of expressiveness and efficiency which allows to apply them in
real-world scenarios. In this paper, we suggest to employ the recently
introduced model of Interval Probabilistic Timed Automata (IPTA) for formal
verification of QoS properties of service-oriented systems. Specifically, we
show that IPTA in contrast to Probabilistic Timed Automata (PTA) are able to
capture the guarantees specified in SLAs directly. A particular challenge in
the analysis of IPTA is the fact that their naive semantics usually yields an
infinite set of states and infinitely-branching transitions. However, using
symbolic representations, IPTA can be analyzed rather efficiently. We have
developed the first implementation of an IPTA model checker by extending the
PRISM tool and show that model checking IPTA is only slightly more expensive
than model checking comparable PTA.
