## 5 Case Study  
To illustrate our approach, we present a case study about monitoring SLA and reducing violations. The relationship between service providers and their consumers is controlled and regulated using SLAs. An SLA includes a set of terms that specify, among others, the expected functional and Quality of Service (QoS) guarantees of the offered service. This contract also specifies penalties that will be applied if its terms are violated. Figure 12: Analysis of the GRR size. Figure 13: Correlation between the model size and the GRR size. Let us consider a provider offering a service that allows consumers to compress their files. This service receives a file from a client and schedules its compression. Once the compression is performed, it delivers the compressed file to the client. Regarding the QoS properties considered in this example, we focus only on the response time. As a penalty, consumers will be compensated with a _0.1 Euro_ discount if the deliverance is delayed after the agreed deadline. As illustrated in Figure 14, we model the behavior of the compression service as a PN. First, the application imports the necessary packages by firing the transitions \(T_{0}\), \(T_{1}\), \(T_{2}\), and \(T_{3}\). The file to be compressed is received when firing \(T_{4}\), and the receiving time is saved using \(T_{5}\). Firing \(T_{6}\) waits for the file turn. Subsequently, the file is compressed using transition \(T_{7}\). Transition \(T_{8}\) obtains the size of the received file, which is used to calculate the cost of the compression operation by \(T_{9}\). Depending on the obtained result, two scenarios may occur. In both scenarios, the time consumed is compared against the pre-agreed time, less than 5. The statements and guards of the transitions are shown in Table 4. \begin{table}
\begin{tabular}{c c c} \hline \hline
**Transition** & **Statement** & **Guard** \\ \hline \(T_{0}\) & import os & True \\ \(T_{1}\) & import time & True \\ \(T_{2}\) & from caseStudy import case\_study & True \\ \(T_{3}\) & from compression import compression\_server & True \\ \(T_{4}\) & input\_file = case\_study.receive\_file() & True \\ \(T_{5}\) & received\_time = time.time() & True \\ \(T_{6}\) & case\_study.wait\_turn() & True \\ \(T_{7}\) & output\_file = compression\_server.zip\_lzma(input\_file) & True \\ \(T_{8}\) & file\_size = os.stat(input\_file)\_st\_size/(1024 * 1024) & True \\ \(T_{9}\) & cost = case\_study.estimate\_cost(file\_size) & True \\ \(T_{10}\) & sending\_time = time.time() & True \\ \(T_{11}\) & consumed\_time = sending\_time \(-\) received\_time & True \\ \(T_{12}\) & case\_study.send\_file(output\_file, cost) & consumed\_time \(<5\) \\ \(T_{13}\) & cost = cost \(-\) 0.1 & consumed\_time \(>=5\) \\ \(T_{14}\) & case\_study.send\_file(output\_file, cost) & True \\ \hline \hline \end{tabular}
\end{table} 
Table 4: Statements and guards of the case study transition. Figure 14: Case study—monitoring of SLA violations. Respected SLA: In the first scenario, the expected time consumed is met (i.e., response time \(<\)5). This scenario is executed by firing transition T12 (see Figure 14). This transition sends the compressed file and the cost of the service to the consumer. This situation can be observed in marking \(\{P_{13}\}\). * Violated SLA: In the second scenario, the deliverance is delayed after the expected deadline (i.e., response time \(>=\)5). This scenario is executed by firing transition \(T_{13}\) (see Figure 14). This transition applies a penalty, as specified in the SLA, to the provider by subtracting _0.1 Euro_ from the cost of the compression operation. The transition \(T_{14}\) sends the compressed file and the final cost to the consumer. The situation of the SLA violation can be monitored by observing markings \(\{P_{14}\}\) and \(\{P_{15}\}\). Another way to monitor the SLA violations is to inspect runtime data using the expression evaluator. Figure 15 shows the evaluation of the expression consumed_time >= 5, which is evaluated as True.