# Workflow Trace Profiling and Execution Time Analysis in Quantitative Verification
###### Abstract
But the aforementioned assumption is usually too restricted to interpret the empirical trace data and thus results in inaccurate analysis output. Therefore, we consider an extension to CTMC, namely, _semi-Markov chain_ (SMC), in which the state holding times are determined by general distributions. The execution time of a trace component is naturally formalised by a fundamental measure in SMC, called _first passage times_ (FPTs). It is noteworthy that in some existing work [17; 18] that aggregate workflow makespans from randomised task times, the workflow is represented as a directed acyclic graph (DAG). But loops, which are allowed in SMC (and other models in the Markovian family), are an essential structure used to build workflow models. However, the generality of an SMC results in a serious challenge for its quantitative verification. First, it is impractical to estimate the exact distribution functions of state holding times from empirical trace data. Second, even if those distributions are given, it is extremely hard to compute the probability that FPT falls in an interval for SMC [19]. In view of these difficulties, we maintain a simple mergeable _summary_ of workflow executions (which comprises frequency values and power sum values only), and compute a group of generic statistical parameters, namely _moments_, for FPT. Our core computational method, which is underpinned by a well-established property of SMC [20], resorts to solving a sequence of linear systems in a reasonable size (i.e., the same size as the SMC). We can either use the FPT moments directly as time metrics for trace components or further infer other statistical parameters, such as quantiles, from the FPT moments using the method of moments ([21], Chapter 10.2). In real-world applications, our approach is suitable for performance monitoring in workflow systems such as AWS Step Functions. In particular, our approach can build compact workflow trace profiles from historical data and recent data in a sliding or decaying time window, and produces a broad range of complex time metrics to define a performance baseline and the current performance for monitoring. We also included an empirical evaluation of the computation time for our approach. The main contributions of this paper are summarised as follows:  
* We leverage probabilistic model checking as a trace profiling approach to formally analyse the complex time metrics for workflow systems. * We present an efficient method to compute the FPT moments in SMC, which complements the existing quantitative verification technique for SMC. * We describe an application of our approach to a notable workflow Web service, namely, AWS Step Functions. The remainder of the paper is organised as follows: Section 2 presents the background of our problem in the time analysis of workflow trace components. Section 3 presents an overview of our approach. Sections 4 and 5 present the technical details, namely, the model building process and the core time analysis method, respectively. Section 6 describes an application of our approach to a real-world workflow system. Section 7 discusses the related work. Finally, Section 8 concludes the paper.