Advanced

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

Mandrioli, Claudio LU ; Leva, Alberto and Maggio, Martina LU (2018) 2nd IEEE Conference on Control Technology and Applications, CCTA 2018 p.1466-1471
Abstract

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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
2018 IEEE Conference on Control Technology and Applications, CCTA 2018
article number
8511410
pages
6 pages
publisher
Institute of Electrical and Electronics Engineers Inc.
conference name
2nd IEEE Conference on Control Technology and Applications, CCTA 2018
conference location
Copenhagen, Denmark
conference dates
2018-08-21 - 2018-08-24
external identifiers
  • scopus:85056899778
ISBN
9781538676981
DOI
10.1109/CCTA.2018.8511410
project
Testing Autonomous Control-Based Software Systems
language
English
LU publication?
yes
id
b8a8fbd4-0afa-493d-a224-e612ab4cc512
date added to LUP
2018-11-29 13:47:06
date last changed
2021-04-06 02:04:58
@inproceedings{b8a8fbd4-0afa-493d-a224-e612ab4cc512,
  abstract     = {<p>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.</p>},
  author       = {Mandrioli, Claudio and Leva, Alberto and Maggio, Martina},
  booktitle    = {2018 IEEE Conference on Control Technology and Applications, CCTA 2018},
  isbn         = {9781538676981},
  language     = {eng},
  month        = {10},
  pages        = {1466--1471},
  publisher    = {Institute of Electrical and Electronics Engineers Inc.},
  title        = {Dynamic Models for the Formal Verification of Big Data Applications Via Stochastic Model Checking},
  url          = {http://dx.doi.org/10.1109/CCTA.2018.8511410},
  doi          = {10.1109/CCTA.2018.8511410},
  year         = {2018},
}