{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T02:43:14Z","timestamp":1760150594126,"version":"build-2065373602"},"reference-count":31,"publisher":"MDPI AG","issue":"12","license":[{"start":{"date-parts":[[2023,12,12]],"date-time":"2023-12-12T00:00:00Z","timestamp":1702339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Hebei Natural Science Foundation","award":["F2020201018","QN2021020","521000981346"],"award-info":[{"award-number":["F2020201018","QN2021020","521000981346"]}]},{"name":"Science and Technology Research Project of Higher Education in Hebei Province","award":["F2020201018","QN2021020","521000981346"],"award-info":[{"award-number":["F2020201018","QN2021020","521000981346"]}]},{"name":"Advanced Talents Incubation Program of the Hebei University","award":["F2020201018","QN2021020","521000981346"],"award-info":[{"award-number":["F2020201018","QN2021020","521000981346"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information"],"abstract":"<jats:p>Apache Spark is a high-speed computing engine for processing massive data. With its widespread adoption, there is a growing need to analyze its correctness and temporal properties. However, there is scarce research focused on the verification of temporal properties in Spark programs. To address this gap, we employ the code-level runtime verification tool UMC4M based on the Modeling, Simulation, and Verification Language (MSVL). To this end, a Spark program S has to be translated into an MSVL program M, and the negation of the property P specified by a Propositional Projection Temporal Logic (PPTL) formula that needs to be verified is also translated to an MSVL program M1; then, a new MSVL program \u201cM and M1\u201d can be compiled and executed. Whether program S violates the property P is determined by the existence of an acceptable execution of \u201cM and M1\u201d. Thus, the key issue lies in how to formalize model Spark programs using MSVL programs. We previously proposed a solution to this problem\u2014using the MSVL functions to perform Resilient Distributed Datasets (RDD) operations and converting the Spark program into an MSVL program based on the Directed Acyclic Graph (DAG) of the Spark program. However, we only proposed this idea. Building upon this foundation, we implement the conversion from RDD operations to MSVL functions and propose, as well as implement, the rules for translating Spark programs to MSVL programs based on DAG. We confirm the feasibility of this approach and provide a viable method for verifying the temporal properties of Spark programs. Additionally, an automatic translation tool, S2M, is developed. Finally, a case study is presented to demonstrate this conversion process.<\/jats:p>","DOI":"10.3390\/info14120658","type":"journal-article","created":{"date-parts":[[2023,12,12]],"date-time":"2023-12-12T05:23:22Z","timestamp":1702358602000},"page":"658","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["DAG-Based Formal Modeling of Spark Applications with MSVL"],"prefix":"10.3390","volume":"14","author":[{"given":"Kaixuan","family":"Fan","sequence":"first","affiliation":[{"name":"Cyberspace Security and Computer College, Hebei University, Baoding 071000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Wang","sequence":"additional","affiliation":[{"name":"Cyberspace Security and Computer College, Hebei University, Baoding 071000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2023,12,12]]},"reference":[{"key":"ref_1","first-page":"669","article-title":"Performance analysis of distributed computing frameworks for big data analytics: Hadoop vs. spark","volume":"24","author":"Ketu","year":"2020","journal-title":"Comput. Sist."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1108\/IJICC-01-2022-0004","article-title":"A comprehensive bibliometric analysis of Apache Hadoop from 2008 to 2020","volume":"16","author":"Zhang","year":"2023","journal-title":"Int. J. Intell. Comput. Cybern."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/2934664","article-title":"Apache spark: A unified engine for big data processing","volume":"59","author":"Zaharia","year":"2016","journal-title":"Commun. ACM"},{"key":"ref_4","unstructured":"Chambers, B., and Zaharia, M. (2018). Spark: The Definitive Guide: Big Data Processing MADE Simple, O\u2019Reilly Media."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"1101","DOI":"10.1016\/j.asej.2020.06.009","article-title":"Analysis of hadoop MapReduce scheduling in heterogeneous environment","volume":"12","author":"Kalia","year":"2021","journal-title":"Ain Shams Eng. J."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1186\/s13677-023-00520-9","article-title":"MapReduce scheduling algorithms in Hadoop: A systematic study","volume":"12","author":"Hedayati","year":"2023","journal-title":"J. Cloud Comput."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.procs.2015.04.108","article-title":"Hadoop, MapReduce and HDFS: A developers perspective","volume":"48","author":"Ghazi","year":"2015","journal-title":"Procedia Comput. Sci."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1016\/j.isprsjprs.2015.11.006","article-title":"Rethinking big data: A review on the data quality and usage issues","volume":"115","author":"Liu","year":"2016","journal-title":"Isprs J. Photogramm. Remote. Sens."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Wang, M., Tian, C., and Duan, Z. (2017, January 20\u201328). Full regular temporal property verification as dynamic program execution. Proceedings of the 2017 IEEE\/ACM 39th International Conference on Software Engineering Companion (ICSE-C), Buenos Aires, Argentina.","DOI":"10.1109\/ICSE-C.2017.98"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"1101","DOI":"10.1109\/TR.2018.2876333","article-title":"Verifying full regular temporal properties of programs via dynamic program execution","volume":"68","author":"Wang","year":"2018","journal-title":"IEEE Trans. Reliab."},{"key":"ref_11","unstructured":"Duan, Z. (1996). An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming. [Ph.D. Thesis, Newcastle University]."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Duan, Z. (2005). Temporal Logic and Temporal Logic Programming, Science Press.","DOI":"10.1007\/11562931_27"},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.tcs.2017.07.032","article-title":"A compiler for MSVL and its applications","volume":"749","author":"Yang","year":"2018","journal-title":"Theor. Comput. Sci."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/j.tcs.2016.02.037","article-title":"A mechanism of function calls in MSVL","volume":"654","author":"Zhang","year":"2016","journal-title":"Theor. Comput. Sci."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","article-title":"A decision procedure for propositional projection temporal logic with infinite models","volume":"45","author":"Duan","year":"2008","journal-title":"Acta Inform."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","article-title":"A practical decision procedure for propositional projection temporal logic with infinite models","volume":"554","author":"Duan","year":"2014","journal-title":"Theor. Comput. Sci."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Yang, X., and Wang, X. (2021, January 5\u20136). A Practical Method based on MSVL for Verification of Social Network. Proceedings of the 2021 8th International Conference on Dependable Systems and Their Applications (DSA), Yinchuan, China.","DOI":"10.1109\/DSA52907.2021.00058"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Zhao, L., Wu, L., Gao, Y., Wang, X., and Yu, B. (2022, January 4\u20135). Formal Modeling and Verification of Convolutional Neural Networks based on MSVL. Proceedings of the 2022 9th International Conference on Dependable Systems and Their Applications (DSA), Wulumuqi, China.","DOI":"10.1109\/DSA56465.2022.00046"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Wang, M., and Li, S. (2021, January 1). Formalizing Spark Applications with MSVL. Proceedings of the International Workshop on Structured Object-Oriented Formal Language and Method, Singapore.","DOI":"10.1007\/978-3-030-77474-5_13"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Luo, N., Yu, Z., Bei, Z., Xu, C., Jiang, C., and Lin, L. (2016, January 16\u201318). Performance modeling for spark using svm. Proceedings of the 2016 7th International Conference on Cloud Computing and Big Data (CCBD), Macau, China.","DOI":"10.1109\/CCBD.2016.034"},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Grossman, S., Cohen, S., Itzhaky, S., Rinetzky, N., and Sagiv, M. (2017, January 24\u201328). Verifying equivalence of spark programs. Proceedings of the Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany. Part II 30.","DOI":"10.1007\/978-3-319-63390-9_15"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Beckert, B., Bingmann, T., Kiefer, M., Sanders, P., Ulbrich, M., and Weigl, A. (2018, January 18\u201319). Relational equivalence proofs between imperative and MapReduce algorithms. Proceedings of the Verified Software. Theories, Tools, and Experiments: 10th International Conference, VSTTE 2018, Oxford, UK. Revised Selected Papers 10.","DOI":"10.1007\/978-3-030-03592-1_14"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Yin, J., Zhu, H., Fei, Y., and Fang, Y. (2019, January 3\u20135). Modeling and Verifying Spark on YARN Using Process Algebra. Proceedings of the 2019 IEEE 19th International Symposium on High Assurance Systems Engineering (HASE), Hangzhou, China.","DOI":"10.1109\/HASE.2019.00039"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s00165-020-00505-4","article-title":"Using formal verification to evaluate the execution time of Spark applications","volume":"32","author":"Baresi","year":"2020","journal-title":"Form. Asp. Comput."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"e1809","DOI":"10.1002\/stvr.1809","article-title":"TRANSMUT-Spark: Transformation mutation for Apache Spark","volume":"32","author":"Musicante","year":"2022","journal-title":"Softw. Testing, Verif. Reliab."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., and Podelski, A. (2015, January 18\u201324). Fairness modulo theory: A new approach to LTL software model checking. Proceedings of the Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA. Proceedings Part I 27.","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., and Piterman, N. (2016, January 2\u20138). T2: Temporal property verification. Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands. Proceedings 22.","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Cook, B., Khlaaf, H., and Piterman, N. (2015, January 18\u201324). On automation of CTL* verification for infinite-state systems. Proceedings of the International Conference on Computer Aided Verification, San Francisco, CA, USA.","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Cook, B., and Koskinen, E. (2011, January 26\u201328). Making prophecies with decision predicates. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Austin, TX, USA.","DOI":"10.1145\/1926385.1926431"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","article-title":"Framed temporal logic programming","volume":"70","author":"Duan","year":"2008","journal-title":"Sci. Comput. Program."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"762","DOI":"10.1007\/s11704-016-6059-4","article-title":"MSVL: A typed language for temporal logic programming","volume":"11","author":"Wang","year":"2017","journal-title":"Front. Comput. Sci."}],"container-title":["Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2078-2489\/14\/12\/658\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T21:37:12Z","timestamp":1760132232000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2078-2489\/14\/12\/658"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,12]]},"references-count":31,"journal-issue":{"issue":"12","published-online":{"date-parts":[[2023,12]]}},"alternative-id":["info14120658"],"URL":"https:\/\/doi.org\/10.3390\/info14120658","relation":{},"ISSN":["2078-2489"],"issn-type":[{"type":"electronic","value":"2078-2489"}],"subject":[],"published":{"date-parts":[[2023,12,12]]}}}