{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:25:34Z","timestamp":1760145934053,"version":"build-2065373602"},"reference-count":42,"publisher":"MDPI AG","issue":"9","license":[{"start":{"date-parts":[[2024,9,3]],"date-time":"2024-09-03T00:00:00Z","timestamp":1725321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Future Internet"],"abstract":"<jats:p>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-Makrov 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.<\/jats:p>","DOI":"10.3390\/fi16090319","type":"journal-article","created":{"date-parts":[[2024,9,3]],"date-time":"2024-09-03T09:56:42Z","timestamp":1725357402000},"page":"319","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Workflow Trace Profiling and Execution Time Analysis in Quantitative Verification"],"prefix":"10.3390","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2087-4894","authenticated-orcid":false,"given":"Guoxin","family":"Su","sequence":"first","affiliation":[{"name":"School of Computing and Information Technology, University of Wollongong, Wollongong, NSW 2522, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4776-5292","authenticated-orcid":false,"given":"Li","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Big Data & Software Engineering, Chongqing University, Chongqing 400044, China"}]}],"member":"1968","published-online":{"date-parts":[[2024,9,3]]},"reference":[{"key":"ref_1","unstructured":"van Der Aalst, W., Van Hee, K.M., and van Hee, K. (2004). Workflow Management: Models, Methods, and Systems, MIT Press."},{"key":"ref_2","unstructured":"AWS Step Functions (2019, August 24). AWS Step Functions Developer Guide. Available online: https:\/\/docs.aws.amazon.com\/step-functions\/latest\/dg\/welcome.html."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Andrade, H.C.M., Gedik, B., and Turaga, D.S. (2014). Fundamentals of Stream Processing: Application Design, Systems, and Analytics, Cambridge University Press.","DOI":"10.1017\/CBO9781139058940"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Cohen, E., and Strauss, M. (2003, January 12\u201317). Maintaining time-decaying stream aggregates. Proceedings of the 22nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, Philadelphia, PA, USA.","DOI":"10.1145\/773153.773175"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Wang, G., Zhang, X., Tang, S., Wilson, C., Zheng, H., and Zhao, B.Y. (2017). Clickstream user behavior models. ACM Trans. Web, 11.","DOI":"10.1145\/3068332"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1109\/TR.2004.823851","article-title":"Robustness of the Markov-chain model for cyber-attack detection","volume":"53","author":"Ye","year":"2004","journal-title":"IEEE Trans. Reliab."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.is.2015.04.004","article-title":"Prediction of business process durations using non-Markovian stochastic Petri nets","volume":"54","author":"Weske","year":"2015","journal-title":"Inf. Syst."},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Katoen, J.P. (2016, January 5\u20138). The Probabilistic Model Checking Landscape. Proceedings of the 31th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201916, New York, NY, USA.","DOI":"10.1145\/2933575.2934574"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1109\/TSE.2010.92","article-title":"Dynamic QoS management and optimization in service-based systems","volume":"37","author":"Calinescu","year":"2011","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Moreno, G.A., Garlan, D., and Schmerl, B. (2016). Analyzing latency-aware self-adaptation using stochastic games and simulations. ACM Trans. Auton. Adapt. Syst., 10.","DOI":"10.1145\/2774222"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","article-title":"Supporting self-adaptation via quantitative verification and sensitivity analysis at run time","volume":"42","author":"Filieri","year":"2016","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1109\/TSE.2020.2996033","article-title":"Quantitative Verification for Monitoring Event-Streaming Systems","volume":"48","author":"Su","year":"2022","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Mangi, F.A., Su, G., and Zhang, M. (2023). Statistical Model Checking in Process Mining: A Comprehensive Approach to Analyse Stochastic Processes. Future Internet, 15.","DOI":"10.3390\/fi15120378"},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Kulkarni, V.G. (2016). Modeling and Analysis of Stochastic Systems, Chapman and Hall\/CRC.","DOI":"10.1201\/9781315367910"},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Su, G., Chen, T., Feng, Y., and Rosenblum, D.S. (2017, January 20\u201328). ProEva: Runtime Proactive Performance Evaluation Based on Continuous-time Markov Chains. Proceedings of the 39th International Conference on Software Engineering, ICSE\u2019 17, Piscataway, NJ, USA.","DOI":"10.1109\/ICSE.2017.51"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","article-title":"Model-checking algorithms for continuous-time Markov chains","volume":"29","author":"Baier","year":"2003","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Glatard, T., Montagnat, J., and Pennec, X. (2008, January 19\u201322). A probabilistic model to analyse workflow performance on production grids. Proceedings of the 8th IEEE International Symposium on Cluster Computing and the Grid, Lyon, France.","DOI":"10.1109\/CCGRID.2008.123"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1016\/j.future.2017.01.011","article-title":"Execution time estimation for workflow scheduling","volume":"75","author":"Chirkin","year":"2017","journal-title":"Future Gener. Comput. Syst."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"L\u00f3pez, G.G.I., Hermanns, H., and Katoen, J.P. (2001, January 12\u201314). Beyond memoryless distributions: Model checking semi-Markov chains. Proceedings of the Joint International Workshop von Process Algebra and Probabilistic Methods, Performance Modeling and Verification, Aachen, Germany.","DOI":"10.1007\/3-540-44804-7_4"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1016\/j.spl.2011.08.021","article-title":"The first-passage times of phase semi-Markov processes","volume":"82","author":"Zhang","year":"2012","journal-title":"Stat. Probab. Lett."},{"key":"ref_21","unstructured":"Wasserman, L. (2013). All of Statistics: A Concise Course in Statistical Inference, Springer Science & Business Media."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"5484","DOI":"10.1016\/j.ins.2007.07.011","article-title":"A probabilistic approach to modeling and estimating the QoS of web-services-based workflows","volume":"177","author":"Hwang","year":"2007","journal-title":"Inf. Sci."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/TSC.2015.2475957","article-title":"Semi-Markov models of composite web services for their performance, reliability and bottlenecks","volume":"10","author":"Zheng","year":"2015","journal-title":"IEEE Trans. Serv. Comput."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Zheng, H., Yang, J., and Zhao, W. (2016). Probabilistic QoS aggregations for service composition. ACM Trans. Web, 10.","DOI":"10.1145\/2876513"},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"1647","DOI":"10.14778\/3236187.3236212","article-title":"Moment-based quantile sketches for efficient high cardinality aggregation queries","volume":"11","author":"Gan","year":"2018","journal-title":"Proc. VLDB Endow."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Agarwal, P.K., Cormode, G., Huang, Z., Phillips, J.M., Wei, Z., and Yi, K. (2013). Mergeable summaries. ACM Trans. Database Syst., 38.","DOI":"10.1145\/2500128"},{"key":"ref_27","first-page":"343","article-title":"The n-th centered moment of a multiple convolution and its applications to an intercloud gas model","volume":"51","year":"1976","journal-title":"Astron. Astrophys."},{"key":"ref_28","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, The MIT Press."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"780","DOI":"10.1137\/S1052623401399903","article-title":"Optimal inequalities in probability theory: A convex optimization approach","volume":"15","author":"Bertsimas","year":"2005","journal-title":"SIAM J. Optim."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Amalarethinam, D.G., and Selvi, F.K.M. (2012, January 10\u201312). A minimum makespan grid workflow scheduling algorithm. Proceedings of the 2012 International Conference on Computer Communication and Informatics, Coimbatore, India.","DOI":"10.1109\/ICCCI.2012.6158777"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Alrifai, M., Risse, T., and Nejdl, W. (2012). A hybrid approach for efficient Web service composition with end-to-end QoS constraints. ACM Trans. Web, 6.","DOI":"10.1145\/2180861.2180864"},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Pietri, I., Juve, G., Deelman, E., and Sakellariou, R. (2014, January 16\u201321). A performance model to estimate execution time of scientific workflows on the cloud. Proceedings of the 9th Workshop on Workflows in Support of Large-Scale Science, New Orleans, LA, USA.","DOI":"10.1109\/WORKS.2014.12"},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/TSC.2012.27","article-title":"QoS-aware dynamic composition of web services using numerical temporal planning","volume":"7","author":"Zou","year":"2012","journal-title":"IEEE Trans. Serv. Comput."},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"1451","DOI":"10.1007\/s11227-022-04703-0","article-title":"A hybrid bi-objective scheduling algorithm for execution of scientific workflows on cloud platforms with execution time and reliability approach","volume":"79","author":"Rahmani","year":"2023","journal-title":"J. Supercomput."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/32.297939","article-title":"A characterization of the stochastic process underlying a stochastic Petri net","volume":"20","author":"Ciardo","year":"1994","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Meyer, P.J., Esparza, J., and Offtermatt, P. (2019, January 6\u201311). Computing the expected execution time of probabilistic workflow nets. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Prague, Czech Republic.","DOI":"10.1007\/978-3-030-17465-1_9"},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3591205","article-title":"Compositional Safe Approximation of Response Time Probability Density Function of Complex Workflows","volume":"33","author":"Carnevali","year":"2023","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"579","DOI":"10.1007\/s10586-021-03432-y","article-title":"Multi-objective workflow scheduling in cloud computing: Trade-Off between makespan and cost","volume":"25","author":"Belgacem","year":"2022","journal-title":"Cluster Comput."},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"1697","DOI":"10.1002\/spe.3268","article-title":"A probabilistic modeling and evolutionary optimization approach for serverless workflow configuration","volume":"54","author":"Wang","year":"2023","journal-title":"Softw. Pract. Exp."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1109\/TSUSC.2023.3314759","article-title":"Reliability enhancement strategies for workflow scheduling under energy consumption constraints in clouds","volume":"9","author":"Zhang","year":"2024","journal-title":"IEEE Trans. Sustain. Comput."},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1109\/TSE.2015.2468717","article-title":"Probabilistic model checking of regenerative concurrent systems","volume":"42","author":"Paolieri","year":"2016","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1145\/937555.937558","article-title":"Model checking stochastic automata","volume":"4","author":"Bryans","year":"2003","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Future Internet"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-5903\/16\/9\/319\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T15:48:04Z","timestamp":1760111284000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-5903\/16\/9\/319"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,3]]},"references-count":42,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2024,9]]}},"alternative-id":["fi16090319"],"URL":"https:\/\/doi.org\/10.3390\/fi16090319","relation":{},"ISSN":["1999-5903"],"issn-type":[{"type":"electronic","value":"1999-5903"}],"subject":[],"published":{"date-parts":[[2024,9,3]]}}}