Formal verification of timed properties for data-intensive applications

In the past few years, cloud-based enterprise applications, leveraging the so-called data-intensive technologies, have emerged as pervasive solutions for modern computing systems. Their adoption has been motivated by the growing need for systems that are able to collect, process, analyze and store huge quantities of data coming from various sources (social media, sensors, bank transactions, etc.) in a reasonable time. Data-intensive applications (DIAs), taking advantage of those technologies, natively support horizontal scalability, and constitute a significant asset for the production of large-scale software systems. However, the adoption of data-intensive technologies in the small and medium enterprises (SMEs), constituting the vast majority of the European industry, is still slow for a number of reasons, such as the steep learning curve of the technologies, the lack of experience and resources to keep up with such innovation. The definition of methodologies and principles for good software design is, therefore, fundamental to support the development of DIAs. Non-functional (quality) requirements are an aspect of software design that is typically overlooked at design time and turns out to be crucial in later stages of development. Usually expressed in terms of Service Level Agreements (SLAs), if they are not met, further refinements of the applications are needed, resulting in additional costs. Design time quality analysis aims at detecting the presence of potential design flaws that could lead to later quality incidents, fostering the early detection of problems. Different approaches exist for the quality analysis of parallel distributed applications. Performance prediction is arguably the most common and is typically enacted on stochastic models by means of either analytical methods or simulation. A different approach is pursued by formal verification: it performs an exhaustive check on the model of the system to assess whether certain properties are satisfied by the modeled system. This thesis presents a unified model-driven approach for the formal analysis and verification of temporal properties for data-intensive applications. It addresses the computation of the two main classes of DIAs, i. e., streaming and batch processing, by proposing two formal models based on metric temporal logic and analyzable through state-of-the-art solvers. Both formalizations, albeit with relevant differences, capture the computational models of DIAs as DAGs, enriched with the most relevant quality aspects of the applications. We first describe timed counter networks, a formal model capturing the computation of Storm-like streaming applications. The model is devised by extending the CLTLoc metric temporal logic with positive discrete counters, and enables the analysis of properties concerning the growth of the queues of the nodes composing Storm topologies. The model can be automatically analyzed (with some limited modifications) by means of the Zot satisfiability checking tool, but it presents some undecidability issues, therefore we propose an additional check to assess the soundness of the analysis results. Then we present an analogous approach for the formalization of the deadline feasibility problem for Spark batch applications. The model is devised as well in terms of CLTLoc extended with counters, but describes a rather different scenario, in which application runs are finite and the goal of the analysis is to determine whether a specific deadline can be met by the designed application. We also discuss a model reduction strategy that exploits the properties of partially ordered sets to partition the DAG underlying the formal model. Next, we introduce D-VerT, a model-driven tool that allows designers to perform the formal analysis of streaming and batch applications by means of an automated toolchain, starting from suitably annotated UML diagrams. D-VerT embeds the models and analysis devised for Storm and Spark applications, and it automatically translates the UML design diagrams to the corresponding instances of the formal models, which are then fed to a state-of-the-art satisfiability solver. In this way, users with limited expertise of formal methods can benefit from the analysis without directly dealing with the specific formalisms. Experimental evaluation has been carried out over the two kinds of analyses performed by D-VerT. The queue boundedness analysis of Storm applications was shown to capture design flaws leading to memory saturation in some of the nodes of Storm topologies, and provided some important hints to designers. In the case of Spark applications, experiments show that the formal model reflects actual executions of the framework with good accuracy (error with respect to the actual execution time less than 10%). Moreover, the proposed optimization registered significant improvements in terms of time (up to 90%) and memory (up to 45%) needed to perform verification. Future works include further refinements of the formal models to improve their accuracy and performance. For example, the optimization strategy for DAG-based computations could be improved and possibly embedded in the decision procedures implemented by the solvers. We also consider the investigation of new properties and different technologies. Moreover, we plan to extend the experimental analysis to new use cases to have a more extensive evaluation. Finally, we are investigating the introduction of probabilities in our models to also carry out stochastic analysis.

Nel corso degli ultimi anni si è registrata una grande diffusione, specialmente in ambito enterprise, di applicazioni basate su cloud computing che sfruttassero le cosiddette tecnologie data-intensive. Tra i principali motivi della loro adozione vi è una sempre maggiore richiesta di sistemi in grado di raccogliere, elaborare, analizzare e memorizzare enormi quantità di dati provenienti da diverse sorgenti (per esempio, social media, reti di sensori, transazioni bancarie, ecc.) in un tempo ragionevole. Le applicazioni data-intensive, sfruttando queste tecnologie, supportano nativamente la scalabilità orizzontale a livello di infrastruttura e costituiscono un asset strategico per la costruzione di sistemi software su larga-scala. Tuttavia, l’adozione delle tecnologie data-intensive nel caso delle piccole e medie imprese (PMI), le quali costituiscono la grande maggioranza delle realtà aziendali europee, continua a procedere lentamente per una serie di ragioni. Tra queste, spiccano una ripida curva di apprendimento che caratterizza queste tecnologie e la mancanza di esperienza e risorse aziendali per sostenere tale innovazione. La definizione di metodologie e principi per una buona progettazione del software è perciò di fondamentale importanza per supportare lo sviluppo delle applicazioni data-intensive. I requisiti non funzionali (o requisiti di qualità) sono un aspetto spesso trascurato nelle prime fasi di progettazione delle applicazioni, mentre risultano essere di fondamentale importanza nelle fasi successive. Solitamente essi sono espressi in termini di Service Level Agreements (SLAs) e, qualora non dovessero essere rispettati dal sistema implementato, quest’ultimo avrebbe bisogno di ulteriori interventi di miglioramento, che a loro volta si tradurrebbero in costi aggiuntivi. L’analisi della qualità a design-time mira ad identificare il prima possibile la presenza di potenziali difetti di progettazione, che potrebbero condurre a successivi problemi nel garantire sufficienti livelli di qualità del servizio. Esistono diversi approcci per l’analisi della qualità di applicazioni distribuite. Quello che con ogni probabilità è il più comunemente utilizzato è la predizione delle prestazioni, solitamente eseguito su modelli stocastici per mezzo di metodi analitici o simulazione. La verifica formale persegue un approccio differente: essa effettua un’analisi esaustiva del sistema modellato per controllare se esso soddisfi o meno determinate proprietà. Questa tesi presenta un approccio unificato per l’analisi e verifica formale di proprietà temporali relative ad applicazioni data-intensive, seguendo una metodologia model-driven. L’approccio si focalizza sulle componenti di elaborazione dei dati delle due principali classi di applicazioni data-intensive— streaming e batch processing—proponendo due diversi modelli formali basati su una logica temporale con metrica e analizzabili tramite solver automatici che sono allo stato dell’arte. Entrambe le formalizzazioni, seppur con importanti differenze, rappresentano i modelli computazionali delle applicazioni come grafi diretti aciclici (DAG), opportunamente arricchiti, per mezzo di annotazioni, con le caratteristiche non funzionali più significative per le analisi da effettuare. Inizialmente presentiamo le timed counter networks, il modello formale che rappresenta la computazione di applicazioni di streaming basate su Apache Storm. Il modello, che è stato sviluppato estendendo la logica temporale con metrica CLTLoc attraverso l’introduzione di variabili discrete positive (o contatori), rende possibile l’analisi di proprietà riguardanti la crescita delle code nei nodi che costituiscono le cosiddette topologie (applicazioni) Storm. Il modello può essere analizzato automaticamente (a seguito di un numero esiguo di modifiche) per mezzo del tool di satisfiability checking Zot. Tuttavia, a causa del formalismo adottato, sono presenti delle problematiche di non decidibilità, per le quali proponiamo una procedura ulteriore per il controllo della validità dei risultati ottenuti tramite l’analisi. Successivamente, presentiamo un approccio analogo per la formalizzazione del problema di fattibilità di una determinata deadline nel caso di applicazioni batch basate su Apache Spark. Anche questo modello formale è espresso per mezzo di CLTLoc estesa con contatori, ma descrive uno scenario decisamente diverso, nel quale l’orizzonte di esecuzione dell’applicazione è sempre finito, e l’obiettivo dell’analisi è quello di determinare se sia possibile, data l’applicazione modellata ed un dataset in input, completare l’elaborazione dell’intero dataset entro una deadline specifica. Inoltre, discutiamo una strategia per la riduzione delle dimensioni del modello formale, la quale sfrutta le proprietà degli insiemi parzialmente ordinati per partizionare il grafo di esecuzione che è alla base della struttura del modello formale. In seguito, presentiamo D-VerT, un tool model-driven che permette a progettisti e sviluppatori di effettuare l’analisi formale su modelli di applicazioni di streaming e batch processing per mezzo di una toolchain automatizzata, che parte con la definizione dei modelli per mezzo di diagrammi UML. D-VerT incorpora i modelli formali e le proprietà di interesse individuate per applicazioni Storm e Spark, e traduce automaticamente i modelli UML contenenti il design dell’applicazione nelle corrispondenti istanze dei modelli formali, le quali sono direttamente sottoposte a verifica per mezzo di un satisfiability solver. In questa maniera, utenti con una minima conoscenza nel campo dei metodi formali possono usufruire dell’analisi senza dover interagire direttamente con i formalismi adottati per rappresentare i sistemi. La valutazione sperimentale dell’approccio è stata effettuata su entrambe le tipologie di analisi supportate da D-VerT. L’analisi di crescita delle code nelle applicazioni Storm ha mostrato di poter individuare dei difetti di progettazione in grado di portare a saturazione di memoria in alcuni dei nodi delle topologie Storm, fornendo importanti indicazioni agli sviluppatori. Nel caso di applicazioni Spark, gli esperimenti hanno mostrato che il modello formale rispecchia le esecuzioni reali del framework con buona accuratezza (errore rispetto ad esecuzioni reali inferiore al 10%). Inoltre, le ottimizzazioni proposte hanno mostrato miglioramenti significativi in termini di tempo (fino al 90%) e memoria (fino al 45%) necessari per effettuare la verifica. Lavori futuri avranno lo scopo di perfezionare i modelli per migliorare la loro accuratezza e le prestazioni delle loro analisi. Ad esempio, la strategia di ottimizzazione presentata nel caso delle applicazioni Spark potrebbe essere migliorata e possibilmente incorporata delle procedure di decisione implementate dai solver. Inoltre, stiamo considerando di approfondire l’analisi di nuove proprietà e tecnologie, e di estendere l’analisi sperimentale a nuovi casi di studio per avere una valutazione più completa e che tenga maggiormente conto di aspetti come quello dell’usabilità e della scalabilità dell’approccio. Infine, stiamo considerando la possibilità di introdurre aspetti probabilistici nei nostri modelli, così da poter condurre a analisi di tipo stocastico.