A Formal Semantics for a Quality of Service Contract Language

Current interests in the context of system development include non-functional aspects of an application and the quality of the service (QoS) it provides. In video on demand applications, for instance, properties such as delay, bandwidth and CPU utilization are monitored in order to identify if they are within acceptable limits. In our approach, non-functional requirements are described by contracts. A contract specifies acceptable variations on the availability of these properties and how service replacement can be negotiated to keep the QoS of the application within the acceptable limits. In this paper we give an operational semantics for QoS contracts and report its implementation in a prototype tool that allows us to execute and analyze QoS contracts. The QoS Tool, our prototype, transforms QoS contract descriptions into modular structural operational semantics (MSOS) specifications. MSOS specifications are executable and analyzable in the Maude MSOS Tool, which uses efficient rewriting to execute, search and model checking MSOS specifications. We exemplify how the QoS Tool can be used by analyzing a video on demand application against real data.