# Workflow Trace Profiling and Execution Time Analysis in Quantitative Verification
## 6 Application and Evaluation
### Model Building  
In the following, we explain how to apply our time analysis approach (as depicted Figure 2) to define the performance baseline and current performance based on the JobDeciderWorkflow example in detail. Recall that there are three inputs to our approach, namely (Input I) a transition system as the workflow model, (Input II) a workflow execution summary and (Input III) one or more DFA, which specify the to-be-analysed trace components. For Input I, the transition system (denoted \(\mathcal{W}_{\text{JobDec}}\)) for JobDeciderWorkflow is built from its specification in the Amazon States Language. There are seven types of states in the FSM of AWS Step Functions, namely Task, Choice, Fail, Succeed, Pass, Wait and Parallel. In the model building, we need to decide the level of abstraction. In AWS Step Functions, when a Lambda Task state (i.e., a Task state that runs a Lambda function) is traversed, the following five low-level events are created (in order): \"TaskStateEntered\", \"LambdaFunctionScheduled\", \"LambdaFunctionStarted\", \"LambdaFunctionSucceeded\" and \"TaskStateExited\". Thus, \(\mathcal{W}_{\text{JobDec}}\) includes five low-level states for each Lambda Task state in the \"Run Job in Parallel\" step. Alternatively, we can consider all steps in JobDeciderWorkflow (including the Task states) as single abstract states in \(\mathcal{W}_{\text{JobDec}}\). Another problem is the parallel states in the FSM, which if directly translated to a transition system, result in a state explosion: The composition of \(N\) parallel Lambda Task states results in \(5^{N}\) lower-level states. However, since our objective is time analysis, we can model the parallel threads with non-deterministic last-completed threads (c.f., Section 4.1). When an execution trace traverses the step \"Run Job in Parallel\", the traverse time is determined by the thread that takes the longest time to complete the part of job. Thus, the step \"Run Job in Parallel\" can be modelled with no more than \(5N\) states in \(\mathcal{W}_{\text{JobDec}}\). For Input II, the statistical values in the execution summary are the frequencies of transitions and the power sums of time intervals (as specified in Section 4.2), which are calculated from the execution traces. The log data of execution traces is available in AWS Step Functions. In particular, the getExecutionHistory API ([[https://docs.aws.amazon.com/step-functions/latest/apireference/API_Operations.html](https://docs.aws.amazon.com/step-functions/latest/apireference/API_Operations.html)]([https://docs.aws.amazon.com/step-functions/latest/apireference/API_Operations.html](https://docs.aws.amazon.com/step-functions/latest/apireference/API_Operations.html)) accessed on 1 June 2024) of AWS Step Functions returns a list of (raw) timestamped trace events for a specific workflow execution. We filter the execution traces where the timestamps of the last events fall into a prescribed time window and then remove the unnecessary events in the following two steps: First, we remove the events that do not belong to the last-completed threads. For example, if \"Run Part-1\" takes the longest time to complete in a trace, we remove all the events related to \"Run Part-2\", \"Run Part-3\",..., and \"Run Part-N\" in the same trace. Second, based on the modelling abstraction level, we may also need to remove the unnecessary low-level events. For example, if we adopt the high-level modelling for \(\mathcal{W}_{\text{JobDec}}\), among the aforementioned five low-level events for each Lambda Task state, we retain \"TaskStateEntered\" only and remove the other four. After removing the unnecessary events, we can replay the traverses of paths in \(\mathcal{W}_{\text{JobDec}}\) and calculate the values of frequencies and power sums, where the detailed method of calculation is presented in Section 4.2.