Modeling and verification of big data computation

In the last decades electronics devices have become always more pervasive in every aspect of human life. Those devices constantly generate data and those data contain information. Being able to store those unprecedented data volumes and to process them in order to retrieve useful information is the so-called challenge of Big Data. This is done through specific software and hardware. Those tools are very complex and exploit the computational power of clusters that can be constituted by dozens of computers. Controlling the behavior of those artifacts is a non-trivial task and it is necessary in order to effectively and efficiently use the involved resources. In this context we propose a systemic approach based on modeling the first-principles of those tools, next for what concerns the analysis of the retrieved model we propose the use of model-checking. Model-checking consists in defining systems and properties in specific languages that allow for automated verification of the defined properties on the given systems. Results show that our model captures the dynamics of those systems, examples of which kind of properties we can now verify are then provided.

Negli ultimi decenni l’utilizzo di dispositivi elettronici è diventato sempre più pervasivo in ogni aspetto della nostra vita quotidiana. Questi dispositivi generano continuamente dati e questi dati contengono informazioni. La capacità di immagazzinare e gestire questi volumi di dati senza precedenti e di processarli per ottenere informazioni è la sfida comunemente nota oggi come Big Data. Per fare ciò vengono usati hardware e software specifici molto complessi che usano le potenzialità offerte da sistemi di calcolo costituiti da anche molte decine di macchine. Controllare questi sistemi presenta molte difficoltà ed è necessario per poterli sfruttare in maniera sia efficace che efficiente. Con questa tesi proponiamo un approccio sistemico per modellare il problema basato sull’idea di catturarne i principi primi che ne governano il funzionamento. Invece, per quanto riguarda l’analisi delle proprietà del sistema, proponiamo l’utilizzo del model checking. Il model-checking consiste nel utilizzo di specifici linguaggi per descrivere sistemi e proprietà tali per cui ne è poi possibile una verifica automatica. I risultati mostrano che il modello proposto cattura la dinamica di questi sistemi; successivamente sono mostrati esempi di quali proprietà si possono adesso verificare.