DAG-Based Formal Modeling of Spark Applications with MSVL
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2023-12-01
|
| Series: | Information |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2078-2489/14/12/658 |
| _version_ | 1797380647068631040 |
|---|---|
| author | Kaixuan Fan Meng Wang |
| author_facet | Kaixuan Fan Meng Wang |
| author_sort | Kaixuan Fan |
| collection | DOAJ |
| description | 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 “M and M1” can be compiled and executed. Whether program S violates the property P is determined by the existence of an acceptable execution of “M and M1”. Thus, the key issue lies in how to formalize model Spark programs using MSVL programs. We previously proposed a solution to this problem—using 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. |
| first_indexed | 2024-03-08T20:40:15Z |
| format | Article |
| id | doaj.art-d5dcc1e6a68b4c9f9f63c65cd9379db9 |
| institution | Directory Open Access Journal |
| issn | 2078-2489 |
| language | English |
| last_indexed | 2024-03-08T20:40:15Z |
| publishDate | 2023-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Information |
| spelling | doaj.art-d5dcc1e6a68b4c9f9f63c65cd9379db92023-12-22T14:15:56ZengMDPI AGInformation2078-24892023-12-01141265810.3390/info14120658DAG-Based Formal Modeling of Spark Applications with MSVLKaixuan Fan0Meng Wang1Cyberspace Security and Computer College, Hebei University, Baoding 071000, ChinaCyberspace Security and Computer College, Hebei University, Baoding 071000, ChinaApache 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 “M and M1” can be compiled and executed. Whether program S violates the property P is determined by the existence of an acceptable execution of “M and M1”. Thus, the key issue lies in how to formalize model Spark programs using MSVL programs. We previously proposed a solution to this problem—using 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.https://www.mdpi.com/2078-2489/14/12/658SparkMSVLtranslationverificationformalization |
| spellingShingle | Kaixuan Fan Meng Wang DAG-Based Formal Modeling of Spark Applications with MSVL Information Spark MSVL translation verification formalization |
| title | DAG-Based Formal Modeling of Spark Applications with MSVL |
| title_full | DAG-Based Formal Modeling of Spark Applications with MSVL |
| title_fullStr | DAG-Based Formal Modeling of Spark Applications with MSVL |
| title_full_unstemmed | DAG-Based Formal Modeling of Spark Applications with MSVL |
| title_short | DAG-Based Formal Modeling of Spark Applications with MSVL |
| title_sort | dag based formal modeling of spark applications with msvl |
| topic | Spark MSVL translation verification formalization |
| url | https://www.mdpi.com/2078-2489/14/12/658 |
| work_keys_str_mv | AT kaixuanfan dagbasedformalmodelingofsparkapplicationswithmsvl AT mengwang dagbasedformalmodelingofsparkapplicationswithmsvl |