# Workflow Trace Profiling and Execution Time Analysis in Quantitative Verification
###### Abstract  
Workflows orchestrate a collection of computing tasks to form a complex workflow logic. Different from the traditional monolithic workflow management systems, modern workflow systems often manifest high throughput, concurrency and scalability. As service-based systems, execution time monitoring is an important part of maintaining the performance for those systems. We developed a trace profiling approach that leverages quantitative verification (also known as _probabilistic model checking_) to analyse complex time metrics for workflow traces. The strength of probabilistic model checking lies in the ability of expressing various temporal properties for a stochastic system model and performing automated quantitative verification. We employ _semi-Markov chains_ (SMCs) as the formal model and consider the _first passage times_ (FPT) measures in the SMCs. Our approach maintains simple mergeable data _summaries_ of the workflow executions and computes the _moment_ parameters for FPT efficiently. We describe an application of our approach to AWS Step Functions, a notable workflow web service. An empirical evaluation shows that our approach is efficient for computer high-order FPT moments for sizeable workflows in practice. It can compute up to the fourth moment for a large workflow model with 10,000 states within 70 s.  
AWS Step Functions; execution time; probabilistic model checking; profiling; semi-Markov chain; workflow +
Footnote †: journal: _Future Internet_  
a _temporal pattern_. The time metrics for trace components can provide more pertinent information to establish a monitoring plan for workflow systems. In general, there are two approaches used to analyse execution traces. Event stream processing [3; 4] is a technique of continuously querying timestamped event logs, which contain low-level and precise footprints of the traces. However, ingesting the telemetry (probably after a cleaning step) from a high-throughput system to a processing platform is not cost-effective. Sampling can alleviate the cost by randomly selecting a portion of data to process, but it comes with the price of lowered accuracy. In contrast, _trace profiling_ is a model-based technique used to build and maintain a statistical profile of the traces. Compared with the set of concrete traces, a profile model is compact and contains rich trace information to be analysed further. In particular, temporal (or behavioural) profiling, which employs models preserving the temporal orders of events, is adopted in various problem domains (e.g., clickstream analysis [5], intrusion detection [6] and process mining [7]). Following the trace profiling approach, we leverage _probabilistic model checking_[8] to analyse time metrics for trace components in workflows. Probabilistic model checking, which is a formal technique of quantitative verification, has been applied to address different problems in software engineering, including Quality-of-Service (QoS) management [9], self-adaptive systems [10; 11], event-streaming systems [12] and business workflows [13]. One main strength of this technique is the ability of expressing a wide range of temporal properties for a system model in the Markovian model family [14] and performing verification in an automated way. As our focus is on time analysis, the Markovian model of workflow profiles should encode not only the _state transition probabilities_ but also the _state holding times_. Moreover, because of the uncertain workload and environment of the workflow system, it is more reasonable to consider the state holding times as random variables rather than fixed values. If we assume that the state holding times are exponentially distributed, we obtain a _continuous-time Markov chain_ (CTMC), which is a widely-adopted model in performance analysis [15]. Based on the memoryless properties of exponential distributions, we can perform automated verification on CTMC using the well-established methods of numerical computation [16].