Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking

Research output: Chapter in Book/Report/Conference proceedingPaper in conference proceeding

Standard

Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking. / Mandrioli, Claudio; Leva, Alberto; Maggio, Martina.

2018 IEEE Conference on Control Technology and Applications, CCTA 2018. Institute of Electrical and Electronics Engineers Inc., 2018. p. 1466-1471 8511410.

Research output: Chapter in Book/Report/Conference proceedingPaper in conference proceeding

Harvard

Mandrioli, C, Leva, A & Maggio, M 2018, Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking. in 2018 IEEE Conference on Control Technology and Applications, CCTA 2018., 8511410, Institute of Electrical and Electronics Engineers Inc., pp. 1466-1471, 2nd IEEE Conference on Control Technology and Applications, CCTA 2018, Copenhagen, Denmark, 2018/08/21. https://doi.org/10.1109/CCTA.2018.8511410

APA

Mandrioli, C., Leva, A., & Maggio, M. (2018). Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking. In 2018 IEEE Conference on Control Technology and Applications, CCTA 2018 (pp. 1466-1471). [8511410] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/CCTA.2018.8511410

CBE

Mandrioli C, Leva A, Maggio M. 2018. Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking. In 2018 IEEE Conference on Control Technology and Applications, CCTA 2018. Institute of Electrical and Electronics Engineers Inc. pp. 1466-1471. https://doi.org/10.1109/CCTA.2018.8511410

MLA

Mandrioli, Claudio, Alberto Leva, and Martina Maggio "Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking". 2018 IEEE Conference on Control Technology and Applications, CCTA 2018. Institute of Electrical and Electronics Engineers Inc. 2018, 1466-1471. https://doi.org/10.1109/CCTA.2018.8511410

Vancouver

Mandrioli C, Leva A, Maggio M. Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking. In 2018 IEEE Conference on Control Technology and Applications, CCTA 2018. Institute of Electrical and Electronics Engineers Inc. 2018. p. 1466-1471. 8511410 https://doi.org/10.1109/CCTA.2018.8511410

Author

Mandrioli, Claudio ; Leva, Alberto ; Maggio, Martina. / Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking. 2018 IEEE Conference on Control Technology and Applications, CCTA 2018. Institute of Electrical and Electronics Engineers Inc., 2018. pp. 1466-1471

RIS

TY - GEN

T1 - Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking

AU - Mandrioli, Claudio

AU - Leva, Alberto

AU - Maggio, Martina

PY - 2018/10/29

Y1 - 2018/10/29

N2 - Big Data Applications (BDAs) manage so much data to require a cluster of machines for computation and storage. Their execution often has temporal constraints, such as deadlines to process the data. BDAs are executed within Big Data Frameworks (BDFs), that provide mechanisms to automatically manage the complexity of the computation distribution. For a BDA to fulfill its deadline when executed in a BDF, online dynamic resource allocation policies should be in place. The introduction of control for such resource allocation calls for formal verification of the closed-loop system. Model checkers verify the correct behaviour of programs, and in principle they could be used to prove properties on the BDF execution. However, the complexity of BDFs makes it infeasible to directly model the BDAs and BDFs. We propose a formalism to associate the execution of a BDA with afirst-principle dynamic simulation model that can be used for model checking in the place of the real application, making the verification viable in practice. We introduce our formalism, apply it to a well assessed framework, and test its capabilities. We show that our solution is able to capture the dynamics and prove properties of the BDA execution using a stochastic model checker.

AB - Big Data Applications (BDAs) manage so much data to require a cluster of machines for computation and storage. Their execution often has temporal constraints, such as deadlines to process the data. BDAs are executed within Big Data Frameworks (BDFs), that provide mechanisms to automatically manage the complexity of the computation distribution. For a BDA to fulfill its deadline when executed in a BDF, online dynamic resource allocation policies should be in place. The introduction of control for such resource allocation calls for formal verification of the closed-loop system. Model checkers verify the correct behaviour of programs, and in principle they could be used to prove properties on the BDF execution. However, the complexity of BDFs makes it infeasible to directly model the BDAs and BDFs. We propose a formalism to associate the execution of a BDA with afirst-principle dynamic simulation model that can be used for model checking in the place of the real application, making the verification viable in practice. We introduce our formalism, apply it to a well assessed framework, and test its capabilities. We show that our solution is able to capture the dynamics and prove properties of the BDA execution using a stochastic model checker.

U2 - 10.1109/CCTA.2018.8511410

DO - 10.1109/CCTA.2018.8511410

M3 - Paper in conference proceeding

SP - 1466

EP - 1471

BT - 2018 IEEE Conference on Control Technology and Applications, CCTA 2018

PB - Institute of Electrical and Electronics Engineers Inc.

ER -