Automated Validation of Compensable SLAs

Automated Validation of Compensable SLAs Carlos M€ uller , Antonio M. Gutierrez , Pablo Fernandez, Octavio Mart ın-D ıaz , Manuel Resinas , and Antonio Ruiz-Cort es Abstract—A Service Level Agreement (SLA) regulates the provisioning of a service by defining a set of guarantees. Each guarantee sets a Service Level Objective (SLO) on some service metrics, and optionally a compensation that is applied when the SLO is unfulfilled or overfulfilled. Currently, there are software tools and research proposals that use the information about compensations to automate and optimise certain parts of the service management. However, they assume that compensations are well defined, which is too optimistic in some circumstances and can lead to undesirable situations. In this article we discuss about the notion of validity of guarantees with a compensation, which we refer to as compensable guarantees (CG). We describe an abstract model of CGs and we provide a technique that leverages constraint satisfaction problem solvers to automatically validate them. We also present a materialisation of the model of CGs in iAgree, a language to specify SLAs and a tooling support that implements our whole approach. An assessment over 319 CGs taken from 24 real-world SLAs suggests that the expressiveness and effectiveness of our proposal can pave the way for using CGs in a safer and more reliable way. Index Terms—Analysis, compensation, CSP, penalty, reward, SLA, validation, WS–agreement Ç 1INTRODUCTION INrecent years the use of Service Level Agreements (SLAs) in Information Systems is in continuous rise. They are widely used by the industry in situations where consumers and providers need or desire to explicitly express certain guarantees over the service provisioning. By means of guarantee terms in the SLA [1], one party (herein after the guarantor) guarantees to another party (herein after the beneficiary) the fulfilment of a Service Level Objective (SLO). For instance, Amazon as provider of its Elastic Compute Cloud Service (AWS EC2) [2] has a term that guarantees its consumers an SLO such that availability 99:95%. More often than not, guarantee terms of real–world SLAs have associated one or more compensations that represent the consequences of unfulfilling (penalties) or overfulfilling (rewards) the SLO. For instance, Amazon is penalised with a 10 percent in service credits if the availability of AWS EC2 drops below 99.95 percent. In other scenarios, a provider may be rewarded when the service provided overfulfils the SLO, i.e., providing a better service level than fixed by the SLO fulfilment. In a previous work we coined the concept of Compensable SLAs [3] to refer to SLAs that include at least either a penalty or a reward. Given the potential economic impact of compensations, it is of the utmost importance to validate that they are well defined in order to avoid undesirable consequences, specially if the action derived from the compensation is automated. For instance, while defining compensations it is desirable to set a limit for the maximum compensation that can be applied if the SLO is not fulfilled. Amazon does so by establishing that they compensate consumers of the AWS EC2 up to a limit of the 30 percent of the monthly bill. Such a limit helps to avoid mistakes like an unbounded, automated penalty that was discarded in 2005 by the UK Royal Mail company after causing a loss of £280 million in one year and a half. 1 However, despite the importance of checking the validity of compensations, it has not been dealt with by current research proposals that use some form of compensation in their SLAs [4], [5], [6], [7], [8], [9], [10], [11], [12], [13], [14], [15], [16], [17], [18], [19]. Instead, they mostly focus on the optimisations of service costs by finding a trade-off between compensation and operation costs or on the automation of several parts of compensation management. These approaches assume that compensations are well defined, which is a too optimistic assumption and the cause of undesirable situations such as the aforementioned UK Royal Mail example. In this paper, we aim at answering the question “How can compensations be automatically validated?” To this end, we build on the compensable SLA model proposed in [3] to provide an automated technique to validate compensable SLAs. Furthermore, we also present a tooling support that implements our validation technique. Our proposal has been evaluated by modelling and analysing the compensations of 24 SLAs of real-world scenarios including 319 guarantee terms. As a result, our technique has proven to be useful for detecting mistakes that are typically derived not only from the manual specification of SLAs in natural language, but also from the complex nature of compensation definitions. This article is structured as follows: Section 2 introduces two motivating real-world scenarios that are used as running examples in the other sections. In Sections 3 and 4 we present The authors are with the E.T.S. Ingenier ıa Inform atica, University of Seville, Sevilla 41012, Spain. E-mail: {cmuller, amgutierrez, pablofm, omartindiaz, resinas, aruiz}@us.es. Manuscript received 9 Feb. 2018; revised 16 Nov. 2018; accepted 3 Dec. 2018. Date of publication 7 Dec. 2018; date of current version 8 Oct. 2021. (Corresponding author: Carlos M€ uller.) Digital Object Identifier no. 10.1109/TSC.2018.2885766 1. Page 3 in http://goo.gl/o7gw6B 1306 IEEE TRANSACTIONS ON SERVICES COMPUTING, VOL. 14, NO. 5, SEPTEMBER/OCTOBER 2021 1939-1374 ©2018 IEEE. Personal use is permitted, but republication/redistribution requires IEEE permission. See ht_tps://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. both, the abstract model and validity criteria of the compensation function, and the compensable guarantees, respectively. In Section 5 we explain in detail all issues related to automating the validity checking of compensable guarantees. Our approach is evaluated in Section 6 by analysing realworld compensable SLAs. In Section 7 we analyse the literature to identify related approaches. Finally, in Section 8 we outline some conclusions and future work. 2RUNNING EXAMPLES In this section two of compensable SLAs found in real world scenarios are introduced as running examples: a computing service and a human-driven IT support service. 2.1 AWS EC2 SLA Amazon Web Services (AWS) is a service catalogue that has boosted the use of cloud computing in the industry. Amongst the services offered by AWS, the Elastic Compute Cloud (EC2) represents a widely used Infrastructure as a Service (IaaS). The aim of EC2 is to provide a scalable infrastructure to organizations that either have variable needs or need to grow seamlessly without the investment for an internal data center. In this context, the reliability of a virtualised infrastructure represents a key point for IaaS consumers in order to choose a service like AWS EC2. As a consequence, Amazon has published an SLA for EC2 2 that guarantees the availability of the virtual resources requested by means of the Monthly Uptime Percentage (MUP) service metric. Specifically, it states that MUP will be greater or equal than 99.95 percent. The consequences of not meeting this SLO is defined in two levels: when MUP drops below 99.95 percent and when it drops below 99 percent. Fig. 1 depicts 3 the penalty function [4] of this scenario that is defined as a percentage of discount in the next billing cycle (Service Credit Percentage). 2.2 GNWT SLA The Government of the Northwest Territories (GNWT) of Canada outsources their IT support. Specifically, the demanded services include issues related to: reporting, user support, problem correction, application enhancement, process and application improvement, and other services. They provide a template for establishing an SLA with an external vendor that provides the mentioned kind of IT support with the desired service levels and penalties and rewards for the parties [20]. Four examples of terms with at least a penalty or a reward have been extracted (cf. Fig. 2) from its SLA template. 4 In example GNWT-1, the government demands the delivery of quarterly reports, which must be received in not less than five days before scheduled review meetings under a penalty of 5 percent of monthly invoice for the provider. Example GNWT-2 depicts specific times for different milestones that take place in the resolution of problems classified with severity 1: they imply a critical application function unusable or unavailable and no immediate workaround exists. Specifically, an initial response should be received within 15 minutes, an estimation response should be ready in 2 hours, subsequent responses are expected every 30 minutes, and the problem must be resolved within 4 hours. In this case, a reward for the provider applies if all problems are resolved in less than 2 hours, and a penalty for the provider applies if any of them is resolved in more than 4 hours. An additional clause rewarding when no problem is older than 60 days is included in GNWT-3. Example GNWT-4 includes a term that relates the scheduled project delivery to the real project delivery, which includes a penalty for the provider if the Elapsed Days Percentage until delivery (EDP) is more than 20 percent greater than planned as well as a reward for the provider if the EDP is 20 percent less than planned. Note that, if the latter sentence is taken literally, the reward does not make sense because it would apply if the delivery is exactly 20 percent less than planned and not for an early-delivery that would be more interesting for the government, e.g., 40 percent less than planned. Such a problem can be solved with the automated validation proposed in Section 5. 3COMPENSATION FUNCTIONS A compensation function is defined over a service metric and can represent two different types of compensation: penalty and reward. A penalty represents a compensation from the guarantor to the beneficiary, whereas a reward Fig. 1. Example AWS EC2: Penalties for Amazon as provider. Fig. 2. Compensation actions extracted from the SLA of GNWT. 2. Available at http://aws.amazon.com/es/ec2/sla/ 3. Note that in all functions, a dark point denotes the inclusion of the metric value in the interval and a gray point means the value exclusion. 4. Available at https://goo.gl/m0duhI M€ ULLER ET AL.: AUTOMATED VALIDATION OF COMPENSABLE SLAS 1307 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. represents a compensation from the beneficiary to the guarantor. Next, we provide a rigorous description. 3.1 Core Definitions Definition 1 (Metric Values). Let mbe a metric of the service, which assumes values within a domain Mm. The domain can be numerical or categorical, in which case Mmis constituted by a (possibly infinite) set of values Mm¼fv1;...;v ng.Ifitis numerical, it can be either continuous, i.e., MmR, or discrete, i.e., MmZ The examples in Section 2 show metrics such as MUP, interventions, and urgent interventions, with bounded domains (e.g., MMUP ¼fv2Rj0v100g); and others such as resolution hours, or EDP with unbounded domains (e.g., MResolutionHours ¼R0). Definition 2 (Utility Function). A Utility Function for the metric m, denoted as Um, is defined as a function from Mmto Rthat associates a utility to each of the values; i.e., it defines which metric values in Mmare more interesting for a given party. Utility functions can be defined as decreasing, increasing, constant, or non-monotonic. Fig. 3 shows a decreasing utility in the dotted function for the metric resolution hours of GNWT-2 example; and a non-monotonic utility function for daily hours of high availability, which aims at optimising different customer goals, such as a common office time of 8 hours per day of high availability, or fully 24 hours per day of high availability, which are the two peeks in the non-dotted function 5 . Utility functions do not appear explicitly in the SLAs because the value each party gives to a service metric is part of their private information and they are usually not willing to share this information with other parties. Definition 3 (Utility Precedence). Let Uma utility function defined on metric m, a precedence relation on Mm, denoted as , can be induced in such a way that given any two values v1;v 22Mmis said that v1is less interesting or useful than v2 when Umðv1Þ<U mðv2Þ. Dotted function in Fig. 3 represents the utility of the beneficiary of GNWT-2. A utility precedence that could be induced is that the higher value of resolution hours, the less interesting for the beneficiary (e.g., 42). Definition 4 (Compensation Function). A Compensation Function for the metric m, denoted as CFm, is defined as a function from Mmto a numerical target set Cthat associates a compensation value to each of the values of m.Ccan be either continuous, i.e., CR, or discrete, i.e., CZ. Similarly to utility functions, the compensation functions can be defined as decreasing, increasing, constant, or non-monotonic. As a normalised convention that is aligned with related work [4], [22] we establish positive compensations as penalties (that should be compensated from the guarantor to the beneficiary) and negative compensations as rewards (i.e., beneficiary should compensate guarantor). Fig. 4 shows an example of increasing compensation function taken from the GNWT-2 example. The function denotes: (1) a reward if problems are solved in less than 2 hours; (2) no compensation applies in problems which are solved between 2 and 4 hours, inclusive, and (3) a penalty if the problems are solved in more than 4 hours. Fig. 1 depicts the compensation function of AWS EC2, which does not take negative values, meaning that only penalties are applicable. Definition 5 (Compensation Regions). Let CFmbe a compensation function of a given metric m; up to three compensation regions can be defined by such compensation function, namely: penalised, rewarded, and neutral. PenalisedðCFmÞ¼fvi2MmjCFmðviÞ>0g NeutralðCFmÞ¼fvi2MmjCFmðviÞ¼0g RewardedðCFmÞ¼fvi2MmjCFmðviÞ<0g: Fig. 4 shows these three potential subsets in GNWT-2 example. Thus, 8vi<2in the Figure, viis a rewarded value; 8vi>4in the Figure, viis a penalised value; and 8vij2vi4in the Figure, viis a neutral value. 3.2 Validity Criteria of Compensation Functions Our proposal to define the validity criteria of a Compensation Function relies on the notions of Consistency and Saturability, that we rigorously describe in the following properties. Property 1 (Consistency). Let be Uma utility function for m defined by the beneficiary, a compensation function CFmis said to be consistent w.r.t. Um, denoted as ConsistentðCFm;U mÞ,if the compensation for a less interesting value of the metric is greater than or equal to the compensation for a more interesting value, according to the utility precedence defined by Um, i.e., if it holds: 8v1;v 22Mmv1v2)CFmðv1ÞCFmðv2Þ: Fig. 3. Example of decreasing or non-monotonic utility functions. Fig. 4. Compensation function of GNWT-2 (CFResolutionHours). 5. Example called “horizontal demand” in [21]. 1308 IEEE TRANSACTIONS ON SERVICES COMPUTING, VOL. 14, NO. 5, SEPTEMBER/OCTOBER 2021 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. Let us analyse the consistency of the compensation functions of AWS EC2 and GNWT-4 examples assuming that, in AWS EC2, the beneficiary establishes that the higher the metric value, the more interesting, i.e., the utility function UMUP is monotonically increasing, while in GNWT-4, the lesser the metric value, the less interesting, i.e., the utility function UEDP is monotonically decreasing. In the case of AWS EC2, the decreasing CFMUP depicted in Fig. 1 is consistent w.r.t. the monotonically increasing UMUP. As counterexample, the non-monotonically increasing CFEDP depicted in Fig. 5 is not consistent w.r.t. the UEDP in the GNWT-4 example because an early-delivery in the 40 percent of EDP, that is a less interesting value for the guarantor, implies a higher compensation than 80 percent of EDP. Property 2 (Saturability). A compensation function CFmis said to be saturated w.r.t. a threshold t¼ðtmin;tmaxÞ, where tmin;tmax 2R, denoted as SaturatedðCFm;tÞif the threshold delimits the higher compensation, either penalty or reward, i.e., if the following holds: 8vi2Mm;CFmðviÞ2½tmin;tmax: This property prevents the definition of unbounded compensations, where the boundary is defined by a threshold t. One may think that it would be enough to check that compensations do not grow infinitely. In practice, however, this is often not enough because, although bounded, it does not guarantee that the compensation is reasonable according to the problem domain. For instance, a compensation that grows linearly with the number of minutes of unavailability in a month is bounded because the number of minutes in a month is also bounded. However, in practical terms, such a compensation may be unreasonable for the provider. Therefore, we define the threshold as a way to set a reasonable boundary in a domain-specific manner. Since compensation functions of the running examples are defined as piecewise functions, they are saturated by definition. Property 3 (Validity). Let Umbe a utility function defined for mby the beneficiary, and let tbe a threshold for m,a compensation function CFmis said to be valid, denoted as ValidðCFm;Um;tÞ, if it is consistent w.r.t. Umand saturated w.r.t. t. i.e., if the following holds: ConsistentðCFm;UmÞ^SaturatedðCFm;tÞ: According to this definition, the compensation functions of Figs. 1 and 4 are valid. On the contrary, the compensation function of GNWT-4 example, depicted in Fig. 5, is not consistent and therefore, not valid. 4COMPENSABLE GUARANTEES A guarantee term guarantees the fulfilment of a certain SLO to a beneficiary (e.g., ResolutionHours 4h). When a guarantee term also includes penalties and/or rewards to compensate the unfulfilment and/or overfulfilment of the SLO, it becomes a compensable guarantee term and by extension its containing SLA becomes a compensable SLA [3]. Next, we provide some core definitions to formally define the validity of compensable guarantees. 4.1 Core Definitions Definition 6 (Service Level Objective). Let mbe a service metric, SLOmis said to be Service Level Objective over a metric m, if it represents a predicate over m. Examples of valid SLOs are ResolutionHours 4h, and MUP 99:95%, in GNWT-2 and AWS, respectively. Definition 7 (Fulfilment Regions). Given an SLOmtwo regions over the values of mcan be defined, namely fulfilment and unfulfilment. FulfilmentðSLOmÞ¼fvi2MmjSLOmðviÞg UnfulfilmentðSLOmÞ¼fvi2Mmj:SLOmðviÞg: According to this definition, the fulfilment region of GNWT-2 scenario is ResolutionHours 4h and the unfulfilment region is ResolutionHours >4h. Definition 8 (Compensable Guarantee). A compensable guarantee defined over a metric m, denoted as CGm, is a tuple of the form ðSLOm;CF mÞ, where SLOmis a service level objective and CFmis a compensation function, both defined over the same service metric m.CGm:SLO refers to the SLO of CGm and CGm:CF to the compensation function of CGm. According to this definition, all guarantees in the article are compensable guarantees. Fig. 6 shows a typical compensation function that depicts the relationships between the fulfilment regions delimited by the SLO and the compensation regions defined by the compensation function (cf. Section 3.1). Moreover, as shown in this Figure, it is important to highlight that fulfilment regions are not Fig. 5. Example of inconsistent CF of GNWT-4 (CFEDP). Fig. 6. A generic example of compensable guarantee showing the fulfilment and compensation regions. M€ ULLER ET AL.: AUTOMATED VALIDATION OF COMPENSABLE SLAS 1309 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. necessarily coupled with compensation regions. Specifically, the Figure exemplifies a case in which metric values between tand bare unfulfilled but not penalised, and similarly metric values between aand tare fulfilled but not rewarded. 4.2 Validity Criteria of Compensable Guarantees The validity of a compensable guarantee resides not only in the validity of its compensation function, but also in the existing coherence between the compensation function and the SLO. Considering the coherence as a property, it can be defined as follows. Property 4 (Coherence). A compensable guarantee CGmis said to be coherent, denoted as CoherentðCGmÞ, if it does the fulfilment regions w.r.t. compensation regions, which implies a threefold condition namely, there is no unfulfilled value that is rewarded, no fulfilled value that is penalised, and there is at least one fulfilled value that is neutral, i.e., if the following holds: UnfulfilmentðCGm:SLOÞ\ RewardedðCGm:CFÞ¼? ^FulfilmentðCGm:SLOÞ\PenalisedðCGm:CFÞ¼? ^FulfilmentðCGm:SLOÞ\NeutralðCGm:CFÞ 6¼ ?: According to this property, GNWT-2 compensable guarantee of Fig. 4 is coherent with its SLO (shown in Fig. 2 as ResolutionHours 4) due to all resolution hour in the SLO fulfilment region is in either rewarded region when the SLO is overfulfilled or in the neutral region; and all resolution hour in the unfulfilment region (i.e., ResolutionHours >4Þ is in the penalised region. Based on Properties 3 and 4 we can formalise the validity of a compensable guarantee as follows: Property 5 (Validity of a CG). Let Ube a utility function defined for metric mby the beneficiary, and let tbe a threshold for m, a compensable guarantee CGmis said to be valid, denoted as ValidðCGm;Um;tÞ, if it is coherent, i.e., the SLO and CF are coherent between themselves; and it contains a valid compensation function w.r.t. Umand t. CoherentðCGmÞ^ValidðCGm:CF;Um;tÞ: According to this property, GNWT-2 compensable guarantee of Fig. 4 is valid because it is coherent and its compensation function is valid. 5VALIDITY CHECKING OF COMPENSABLE GUARANTEES Checking whether a compensable guarantee contains any errors become a tedious and time-consuming task, and it is error-prone in itself. Our approach to automate this process is depicted in Fig. 7 and requires a language to specify compensable guarantees. Thus, we propose the use of iAgree [23], a WS–Agreement-based [1] language with precise semantics (cf. Section 5.2). The underlying idea is to leverage offthe-shelf Constraints Satisfaction Problem (CSP) reasoners to automate the analysis of operations; more specifically, to extract information from the CSPs that represents the compensation function of the guarantee specified in iAgree. As shown in Fig. 7, we establish a hierarchy of operations: the Validity properties formalised in Sections 3 and 4 (included in the reduced glossary of Table 1) for CF (Property 3) and CG (Property 5), respectively, are derived from three core operations, namely: Consistency (Property 1), Saturability (Property 2), and Coherence (Property 4). Each core operation can be Fig. 7. Process to automate the validity checking. TABLE 1 Definitions and Properties Glossary Definition Reduced Explanation MmSet of all values for a metric m. UmFunction that associates a utility to each value of m. Precedence Precedence relation denoting that a value of m is less interesting than other. CFmFunction that associates a compensation to each of the values of a metric. Compensation Regions PenalisedðCFmÞ,RewardedðCFmÞ,NeutralðCFmÞ; where the metrics values have an associated penalty, reward, or none, respectively. SLOmA service level over m (i.e., a predicate over m). Fulfilment Regions FulfilmentðSLOmÞ,UnfulfilmentðSLOmÞ; where the metrics values hold and do not hold the SLO predicate, respectively. CG A guarantee that includes either a penalty, a reward, or both. It comprises both, a SLOmand a CFm. Property Reduced Explanation ConsistentðCFm;UmÞA CF is consistent if the compensation for a less interesting value of m is greater than or equal to the compensation for a more interesting value, according to the utility precedence. SaturatedðCFm;tÞA CF whose penalties or rewards are always less than a threshold (t). ValidðCFm;Um;tÞA CF that is consistent and saturated. CoherentðCGÞA CG whose fulfilment and compensation regions make sense (e.g., there is no unfulfilled value that is rewarded, etc). ValidðCGm;Um;tÞA CG that is coherent and its CF is valid. 1310 IEEE TRANSACTIONS ON SERVICES COMPUTING, VOL. 14, NO. 5, SEPTEMBER/OCTOBER 2021 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. expressed in terms of a standard CSP-based reasoning operation (cf. .solve in Fig. 7). This scheme requires to define a mapping between iAgree compensations and CSP denoted as map (CF) in this Figure. 5.1 Inferring Utility Function and Saturability Thresholds As described in Section 3.2, the validity of a compensation function requires knowing besides the compensation function of each compensable guarantee, both, (i) the utility function of the beneficiary for each metric as far of the Consistency property; and (ii) the threshold for the Saturability property. However, these elements are not usually public, and hence, they do not appear in the SLA. Therefore, they must be provided by domain experts during the validity checking. However, although the utility function is not explicitly described in the SLA, its structure can be roughly estimated from the SLO; based on our analysis, this assumption has proved to be useful in order to avoid an explicit utility function definition in most of SLAs found in the industry. After analysing up to 24 SLAs, 95 percent of their 319 compensable guarantees include simple SLOs in the form of metric >target value or metric <target value. Therefore, the intuitive related utility can be described as a monotonic linear function directly proportional (a greater value of the metric is more useful) or inversely proportional (a lower metric value is more useful) to metric values, respectively. For instance, in the SLO: availability 99, the utility function can be described as UavailabilityðxÞ¼x, and in the SLO EDP 120 (cf. SLO of Fig. 8), the utility function can be described as UEDPðxÞ¼x. Therefore, to avoid manual modelling, we apply this simple automatic criteria using the SLO inequation to define the utility function in our tooling. This approach is not valid when there is no explicit SLO, the SLO is specified as an equation instead of an inequation, or the SLO is more complex, but it covers the 95 percent of modelled agreements. In cases where the SLO is defined as an equation (e.g., UnavailableMinutes ¼¼0), the domain expert had to model it, with no side-effects in validation, to the SLO UnavailableMinutes 0, that allows to infer a proper utility function for the metric (the sign of the inequation can be decided based on the metric semantic). This modelling decision is valid in all the analysed scenarios but should be extended for objectives such as deliveryDay ¼Friday; in such cases, in spite formalisation provides support for that, the tools developed would need to be extended since it is required for automatically inferring a utility function. As a potential alternative, if the utility function was provided by the user, then SLOs could be defined as an equation. Regarding the saturability property, there are different situations where the maximum (tmax) and the minimum (tmin) values are defined in the SLA. In some cases, as in Fig. 8, compensation is defined through constant values, 10 and -5, in lines 32 and 37, so the maximum and minimum possible values are in fact saturability thresholds. In cases where there are no explicit thresholds in the SLA and they are not included in analysis (e.g.,: c¼100 DelayDays), the default approach is using the domain of the compensation variable as threshold. Thus, we consider that if the compensation can reach maximum or minimum domain value, it is not saturated. 5.2 iAgree as Specification Language The validity properties identified for compensable guarantees deal with four key elements, namely: service metrics (m), compensable guarantees (CG), service level objectives (SLOs), and compensation functions (CF). In such a context, iAgree already supported with a precise semantics mand SLOs, complementary, as a key contribution of this paper, we extend the support to include CG by means of a formal semantics for CF;thisextensionis detailed in Section 5.3. Fig. 8 depicts an excerpt of the GNWT SLA in iAgree including the GNWT-4 compensable guarantee. Specifically, an iAgree SLA includes two types of elements, namely: a context and a set of terms. The context specifies who the consumer and provider are and defines schemas that specify the domain and unit for the compensations used in the SLA (we refer to the compensation value as cin the following sections; cf. Penalty Invoice Percent, PIP in the example, line 10). The terms are divided into metrics and guarantees. Metrics are specified by means of their schemas, which define their values (m; cf. EDP in the example, line 16). Therefore, schemas can be seen as a function domain that returns the domain of either metrics or compensation defined as domainðmÞ¼Mmand domainðcÞ¼Mc, respectively (e.g., domainðEDPÞ¼½200;...;200, line 20). Guarantees include both: (i) the SLO defined on a service metric (SLOm; cf. EDP <120 in the example, line 24), and (ii) the Compensation Function (CFm). Following the WS–Agreement specification, CFmis defined by specifying penalties and rewards separately. Neutral values are not explicitly specified and include those that are not part of any penalty or reward. For each penalty and reward, the compensation domain is defined by means of element over. Fig. 8. GNWT-4 compensable guarantee term in iAgree syntax. M€ ULLER ET AL.: AUTOMATED VALIDATION OF COMPENSABLE SLAS 1311 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. The definition of the penalty (or reward) part of the compensation function is done as a piecewise function through a set of ðvalue; conditionÞpairs (e.g., ‘10’;EDP 120, lines 32 and 33 in the penalty of the example). According to our definition of CFm, both penalty and reward are defined over the same schema, a penalty schema in our example. It is important to highlight that, based on the analysis of SLAs in the industry (cf. Section 6) two assumptions can be made in our example: first, following our CF definition we use the PIP as the compensation metric assuming a positive value as penalties and negative value as rewards; and second, the usage of piecewise functions proves to be sufficiently expressive to model a wide range of compensations functions in real-world scenarios as shown in Section 6. 5.3 Formal Semantics of iAgree Compensation Functions The primary objective of formalising iAgree compensation functions is to establish a sound basis for an automated support. Therefore, according to the formalisation principles defined by Hofstede et al. [24], the style and target domain should be chosen accordingly (Primary Goal Principle). In our case, we follow a transformational style and we propose CSP as target domain because of two major reasons. First, compensations are specified by means of constraints of their related metrics. Thus, a quite straightforward way to implement the checking of the introduced properties (cf. Sections 3 and 4). Second, similar techniques have been previously applied by the authors [25], [26] to analyse several SLA problems, namely: (i) the conflicts between agreement terms (e.g., to avoid inconsistencies); (ii) the SLA violation (e.g., to detect violations and explain potential causes); and (iii) the compliance between agreements and agreement templates. A CSP is defined as a triple ðV; D; CÞof a set of variables V, their domains Dand a number of constraints C. A solution of a CSP is an assignment of values to the variables in Vfrom their domains in Dso that all the constraints in C are fulfilled. A CSP operation that returns if it has at least one solution is called solve, and there are a number of solvers that automates this CSP operation. Our approach, thus, involves mapping the iAgree CF to a CSP and then using the solve operation of a CSP solver to check the different properties. Next we explain this mapping in detail, summarising it in Table 2. In the following, to refer to the elements in the iAgree document we use the following notation. For each compensable guarantee, CG, in an iAgree document, we will use CG.SLO, CG.CF to refer to its SLO and compensation function, respectively. The compensation function is defined with penalties and rewards, notated as Pand R, respectively. Furthermore, m and c refer to the metric and the compensation variable used in the guarantee. Similarly, and abusing the notation, for each set of penalties that conform the piecewise penalty function P(resp. rewards R), Pcond;n, and Pval;n refer to the n-th condition and the n-th value of the penalty, respectively (resp. Rcond;n,Rval;n for the set of rewards R). Mapping the Compensation Function (CF): Table 2 describes the CSP of a compensation function defined as a set of penalties and rewards. The compensation and the metrics (together with their schemas) in Agree are the variables (and their domains) in this CSP. Each ðvalue;conditionÞpair in penalties or rewards in iAgree is mapped to a constraint of the form condition ) variable ¼¼ value. Hereinafter, we use cto refer to the compensation variable (penalties and rewards could refer to different compensation variables but then, they would be analysed as different compensation functions). By definition in iAgree, the compensation is zero outside the defined penalty and reward expressions so we add an additional constraint with this consideration. Finally, all theseconstraintsarecombinedwithanAND operator. Note that this mapping corresponds to a well-defined piecewise function; as a potential extension, before the presented compensation analysis, we could check whether the compensation is a mathematical well-defined function (e.g., two different penalty values with the same condition cannot exist). The resulting CSP of mapping the compensation function of guarantee GNWT-4 in Figure 8 is as follows: mapðCFEDPÞ ¼ffEDP;PIPg;fint½200::200;int½100::100g; fðEDP 120 )PIP ¼¼ 10ÞAND ðEDP ¼¼ 80 )PIP ¼¼ 5ÞAND NOTðEDP ¼¼ 80 OR EDP 120Þ)ðPIP ¼¼ 0Þgg: This CSP is used to evaluate the analysis operations for the properties of CF and CG, which are described next. 5.4 Automated Checking Operations In this section we explain the automated technique to check the core operations of the proposed properties (cf. Table 3). Note that we stand by: (i) the CF mapping in Table 2 (mapðCFmÞ), (ii) the inferred utility function (Um), and (iii) the inferred saturability thresholds (tmin;tmax). Since core operations are used to check the Validity operations, we have also included them to provide all checking operations. TABLE 2 Compensation Function to CSP 1312 IEEE TRANSACTIONS ON SERVICES COMPUTING, VOL. 14, NO. 5, SEPTEMBER/OCTOBER 2021 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. Operation for Consistency (Property 1). Since CSPs can only solve satisfiability problems (i.e., exists a solution) and we have to check if this property holds for all possible values, we verify this property with the solve operation and verifying that there is not value which solves the inconsistency of the compensation function. That is, there do not exist two different metric values, m1and m2, where m1has higher utility than m2(Um1 and Um2, respectively), but also higher compensation value (c1and c2, respectively). For instance, if the CF is defined on metric EDP, we define two different metrics, EDP1 and EDP2, with the same compensation function (that is duplicating the penalty and rewards conditions for the duplicated metrics). We express this using ra=bðCFÞ, which means that we rename bwith ain CF. The property is evaluated by adding a constraint that relates the two compensations and utilities for these variables so that one variable can have both a higher compensation (i.e., higher penalty) and a higher utility than the other. If the resulting constraints can be solved (i.e., it has a solution) it implies that the function is not consistent. Otherwise, it would mean that there are two values of the metric variable for which one have both higher penalty and higher utility than the other. In our example, a greater delay in delivery is less useful for the customer, this means that the utility function is inversely proportional to the metric EDP. Thus, according to our described utility inference, a possible utility function U could be the negative function of the metric: UEDP ¼EDP, and consequently, the constraint ðUm1>Um2Þreplaced by ð EDP1>EDP2Þin our example. ConsistentðCFEDP;UEDPÞ, NOTðsolveðmapðrEDP1;PIP1=EDP;PIPðCFEDPÞÞ AND mapðrEDP2;PIP2=EDP;PIPðCFEDPÞÞ AND ðPIP1>PIP2ÞAND ð EDP1>EDP2ÞÞÞ; where r1(resp. r2) renames EDP and PIP by EDP1and PIP1(resp. EDP2and PIP2). As this CSP is satisfiable, i.e., solve returns a solution, the example compensation function is inconsistent. This is an effect of a wrong compensation definition, which only rewards when the value for EDP is exactly 80, but does not reward more useful values. For instance, the reward does not apply if a project is delivered one month earlier than planned; but it only applies if it is delivered exactly one week earlier than planned. Operation for Saturability (Property 2). For this property, the operation receives two additional input values, the saturability thresholds, so we only check if the metrics are outside these two values. If they are, then we consider it not saturated. In our example, following a domain expert consideration, 30 and -30 are suitable candidate for saturability thresholds. Thus, the CSP for checking the saturation in the example compensation function is: SaturatedðCFEDP;30;30Þ, NOTðsolveðmapðCFEDPÞANDðPIP >30 OR PIP <30ÞÞÞ: As the compensation variable cannot reach maximum or minimum values in any case (its only possible values are 10, 0 and -5), the problem is not satisfiable and the compensation is therefore saturated. Operation for Validity of Compensation Function (Property 3). This is a derived operation of core consistent and saturated operations. ValidðCFEDP;UEDP;30;30Þ, ConsistentðCFEDP;UEDPÞAND SaturatedðCFEDP;30;30Þ: In our example, the compensation is invalid (it is saturated but not consistent). Operation for Coherence (Property 4). This property involves checking one existentially quantified constraint (it exists at least one value that is neutral and fulfilled), and one universally quantified constraint (no value is fulfilled and penalised or unfulfilled and rewarded at the same time). Therefore, we build and solve two different constraints to evaluate this property. First, if it exists a neutral compensation region for an SLO fulfilled value, and if it does not exist a positive compensation value (penalty) when the SLO is fulfilled or a negative compensation value (reward) when SLO is unfulfilled. The operation to check the coherence between compensation function and the SLO in our example is: CoherentðCGEDPÞ, solveðmapðCGEDP:CFÞAND ðPIP ¼¼ 0 AND EDP <120ÞÞ AND NOTðsolveðmapðCGEDP:CFÞAND ððPIP >0 AND EDP <120Þ OR ðPIP <0 AND NOTðEDP <120ÞÞÞÞÞ: As it exists a neutral compensation when EDP is less than 120 and it does not exist any positive compensation when EDP is less than 120 neither negative when EDP is greater or equal than 120, the compensable guarantee is coherent. Operation for Validity of Compensable Guarantee (Property 5). The compensable guarantee is valid if it is coherent with compensation function (Property 4) and the compensation function is valid (Property 3). Therefore we provide this operation as a derived operation of the core coherent operation and the derived valid compensation operation. ValidðCGEDP;UEDP;30;30Þ, CoherentðCGEDPÞAND ValidðCGEDP:CF;UEDP;30;30Þ: TABLE 3 Automated Core Operations Using Solve Operation of CSPs M€ ULLER ET AL.: AUTOMATED VALIDATION OF COMPENSABLE SLAS 1313 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply. For our example, the compensation function is invalid, hence the compensable guarantee is also invalid. 5.5 Tooling Support In order to assist in the modelling and analysis of properties, an ecosystem of tools has been developed 6 that is composed of (i) an analysis framework, that is implemented using a MiniZinc [27] CSP solver; and (ii) a designer tool that are integrated by means of REST APIs. As shown in Fig. 9, the designer studio (part of the larger framework Governify) provides a GUI that allows modelling and analyzing compensable SLAs: specifically, it is possible to generate workspaces (far left section of the tool) with agreements written in iAgree with a YAML/JSON format (left editor) or using a form that renders the compensation function in a graphical way (right editor). Once the agreement is modelled, a general validity check of compensations is available (bottom right blue button) or an individual operation check for each property identified in Sections 3 and 4 can be invoked (bottom right gray dropdown). The result of the operations is shown in the console of the tool (bottom section) highlighting the logic (true/false) outcome of the operation. In case of properties P1, P2 and P4 a CSP mapping can be shown (blue link in the console) describing the actual MiniZinc CSP that is executed in the engine to solve the property check. Following the micro-service architecture principles, the analysis module exposes a well defined REST API 7 that is divided into two main resources: first, the models resource, that corresponds to the different types of documents allowed as inputs for the analysis (e.g., agreements) and their serialisation formats (currently JSON and YAML). Second, the operations resource, that allocates the different analysis available for a given model. From an internal perspective, the agreement module develops a two stage model transformation process: first, the agreement model is transformed using the mapping rules presented in Section 5.4 into a simplified CSP model composed of variables, domains and constraints; second, the CSP model is serialised into the MiniZinc CSP language. In order to execute the solver, a docker container has been integrated so MiniZinc engine can be invoked dynamically for each file generated. 6EVALUATION IN REAL-WORLD SCENARIOS In this section we describe how we have evaluated our proposal. In particular, the goal of the evaluation was to answer the following research questions: RQ1: How Expressive is our Compensations Model in Comparison to Real-World SLAs? We want to know whether Fig. 9. Screenshot of our designer studio tool. 6. Available at https://isa-group.github.io/2017-12-compensations/ 7. A portal for this API is available at https://goo.gl/zbCG9i 1314 IEEE TRANSACTIONS ON SERVICES COMPUTING, VOL. 14, NO. 5, SEPTEMBER/OCTOBER 2021 Authorized licensed use limited to: Universidad de Sevilla. Downloaded on December 20,2021 at 10:44:02 UTC from IEEE Xplore. Restrictions apply.