@inproceedings{0a4f2b3235324375aa4533ee1dcbcd76,
title = "Modeling and verifying spark on YARN using process algebra",
abstract = "As a programming model, Spark is popularly and widely used in processing and generating large cluster of data sets distributed on large amounts of machines. With its widespread use, its validity and other major properties need to be analyzed in a formal framework. And unfortunately, there is nearly no research conducted to describe the interactions in Spark on YARN. In this paper, we focus on the dominant parts of Spark on YARN and formalize them using Communicating Sequential Processes (CSP) in detail. In the formal model, the processing and function of each component are clearly described. By feeding the models into the model checker Failures Divergence Refinement (FDR), we have verified some crucial properties, including Deadlock Freedom, Divergence Freedom, Robustness and Load- Balancing. Our work demonstrates that Spark on YARN can guarantee important properties in some applications.",
keywords = "Csp, Fdr, Modeling, Spark on yarn, Verification",
author = "Jiaqi Yin and Huibiao Zhu and Yuan Fei and Yucheng Fang",
note = "Publisher Copyright: {\textcopyright}2019 IEEE.; 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019 ; Conference date: 03-01-2019 Through 05-01-2019",
year = "2019",
month = mar,
day = "22",
doi = "10.1109/HASE.2019.00039",
language = "英语",
series = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",
publisher = "IEEE Computer Society",
pages = "208--215",
editor = "Congfeng Jiang and Dongjin Yu and Vu Nguyen",
booktitle = "Proceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019",
address = "美国",
}