Reliability of Run-Time Quality-of-Service Evaluation Using Parametric Model Checking

Run-time Quality-of-Service (QoS) assurance is crucial for business-critical systems. Complex behavioral performance metrics (PMs) are useful but often difficult to monitor or measure. Probabilistic model checking, especially parametric model checking, can support the computation of aggre- gate functions for a broad range of those PMs. In practice, those PMs may be defined with parameters determined by run-time data. In this paper, we address the reliability of QoS evaluation using parametric model checking. Due to the imprecision with the instantiation of parameters, an evaluation outcome may mislead the judgment about requirement violations. Based on a general assumption of run-time data distribution, we present a novel framework that contains light-weight statistical inference methods to analyze the re- liability of a parametric model checking output with respect to an intuitive criterion. We also present case studies in which we test the stability and accuracy of our inference methods and describe an application of our framework to a cloud server management problem.

1. Introduction

With the rise of the service-oriented business model (e.g., cloud computing), it becomes increasingly important to ensure Quality-of-Service (QoS) requirements throughout the period of service provision. One notable example is the service-level agreement (SLA) between a service provider and a client, which usually defines a set of performance metrics (PMs) and their thresholds in qualitative and quantitative terms. According to the PM structure, PMs can be categorized as atomic and composite [19]. Typical examples of atomic PMs are “link failure”, “delay” and “utilization”, which can be determined by direct run-time monitoring. One common form of PM compositions is the aggregation of atomic PMs over a specific time interval, such as “average availability”, “maximum response time” and “top 10%”. Another and more complex form is behavioral aggregation, such as “failure rate in ten consecutive requests” and “expected time to reach maximum queue size”. Extensive research efforts have been dedicated to QoS management in the presence of uncertainty (e.g., [2], [23], [29]).