Trace checking of quantitative properties

Software engineering has dramatically changed over the past decade and many of the changes have challenged our most basic assumptions about the nature of the software products that we develop. The most important realization is that modern software has a very complex interaction with the environment in which it executes and it is often not safe to assume that the behavior of the environment is stable. Designing software that anticipates changes in the environment makes the software itself exhibit dynamic behavior that can only be observed at run time. This asks for verification techniques that complement design-time approaches and puts forward trace checking as a viable complementary choice for verifying modern software. Trace checking is an automatic procedure for evaluating a formal specification over a trace of recorded events produced by a system after execution. The output of the procedure states whether the system behaves according to its specification. The goal of this thesis is to develop general and efficient trace checking procedures that support a broad class of quantitative properties. Quantitative properties can be seen as constraints on quantifiable values observed in an execution of a system. Quantitative properties typically express non-functional requirements, like constraints on resource utilization (e.g., number of computation resources, power consumption, costs), constraints on the runtime characteristics of the environment (e.g., arrival rates, response time), or constraints on the runtime behavior of the system (e.g., timing constraints, QoS, availability, fault tolerance). The first part of the thesis discusses two algorithms that implement the satisfiability procedure for SOLOIST - a specification language based on metric temporal logic (MTL) used to express quantitative properties. We show how a satisfiability procedure can be used to perform trace checking and apply the proposed approach to an extensive case study in the domain of cloud-based elastic systems. The second part of the thesis focuses on the problem of distributed trace checking and provides algorithms that rely on existing distributed computation frameworks (like MapReduce and Spark) to efficiently check SOLOIST specifications over very large traces. The thesis also contributes to the state of the art in MTL trace checking by proposing a novel decomposition technique for MTL formulae. This decomposition provides a scalable way of trace checking formulae with large time intervals. Due to known restrictions of the standard point-based MTL semantics we facilitate the decomposition by proposing an alternative semantics for MTL, called lazy semantics. The new semantics is more powerful than point-based semantics and possesses certain properties that allow us to decompose any MTL formula into an equivalent MTL formula with smaller time intervals.

La disciplina dell'ingegneria del software è cambiata radicalmente nell'ultimo decennio e molti dei cambiamenti hanno stravolto le nostre assunzioni fondamentali sulla natura del software che sviluppiamo. La consapevolezza più importante è che il software moderno ha una complessa interazione con l'ambiente in cui viene eseguito e spesso non si può supporre che il comportamento dell'ambiente sia stabile. La progettazione di software in grado di anticipare i cambiamenti dell'ambiente determina che il software stesso esibisca un comportamento dinamico, osservabile solo in fase di esecuzione. Questo tipo di software richiede tecniche di verifica che siano di complemento agli approcci usati durante lo sviluppo e propone la tecnica di verifica di tracce (trace checking) come una soluzione praticabile e complementare per la verifica del software moderno. La verifica di tracce è una procedura automatica per la valutazione di una specifica formale su una traccia di eventi prodotti dal sistema e salvati dopo l'esecuzione del sistema stesso. L'output di questa procedura indica se il sistema è stato conforme alla sua specifica. L'obiettivo di questa tesi è quello di sviluppare procedure di trace checking che siano generali ed efficienti e che supportino un'ampia classe di proprietà quantitative. Quest'ultime sono dei vincoli su valori quantificabili osservati durante l'esecuzione di un sistema. Questo tipo di proprietà esprime tipicamente requisiti non funzionali, come i vincoli sull'utilizzazione delle risorse (e.g., numero di risorse, consumo di energia, costi), vincoli sulle caratteristiche di esecuzione dell'ambiente (e.g., frequenza delle richieste, tempo di risposta), o vincoli sul comportamento del sistema durante la sua esecuzione (per esempio, vincoli temporali, qualità del servizio, affidabilità, tolleranza ai guasti). La prima parte della tesi descrive due algoritmi che implementano la procedura di soddisfacibilità per SOLOIST - un linguaggio di specifica basato sulla logica temporale con metrica (MTL) ed utilizzato per esprimere proprietà quantitative. La tesi mostra come si possa usare una procedura di soddisfacibilità per eseguire la verifica di tracce e descrive l'applicazione di questa procedura ad un caso di studio nel settore dei sistemi elastici basati su infrastrutture cloud. La seconda parte della tesi si concentra sul problema della verifica distribuita di tracce e descrive algoritmi basati su modelli di calcolo distribuito (come MapReduce e Spark) per la verifica, in modo efficiente, di specifiche SOLOIST su tracce di esecuzione molto grandi. La tesi considera anche il dominio della verifica su tracce di proprietà espresse in MTL e propone una nuova tecnica per la decomposizione di formule MTL. Questa tecnica permette di effettuare la verifica di tracce, in modo scalabile, anche in presenza di formule con intervalli temporali molto ampi. La tecnica di decomposizione proposta supera le limitazioni della semantica standard di MTL attraverso la definizione di una nuova semantica per MTL, chiamata"lazy". Questa nuova semantica è più espressiva della semantica standard e possiede alcune proprietà che permettono di decomporre qualsiasi formula MTL in una formula MTL equivalente con intervalli di tempo più piccoli.