Requirements Verification of Variability-Intensive Systems

objective of this thesis is to devise techniques to verify different properties of Variability-Intensive Systems. By Variability-Intensive System, we refer to a specification from which various systems can be derived. Adaptive systems and software product lines are two important examples of such systems. In the former case, system switches among different configurations at run time, while in the later case, each valid configuration is released as a single product at development time. Incomplete specifications of system behavior, which are incrementally developed during development, are another kind of specifications that evolve over time, and may lead to different releases. We classify variability in two classes: open and closed. Accordingly, the thesis is divided into two main parts, which are dedicated to these two types of systems. Open variability refers to the cases where the specifications of alternatives are unknown, which is the case of incomplete specifications. This is exactly opposite in the case of closed variability for which the specification is complete, that is the case of software product lines. Part II presents a novel approach for specification and verification of incomplete software models against temporal logic properties and in particular CTL. An incomplete model may represent a partial design of a system at early development stages, in which some components are not yet specified. The unknown components can be viewed as variation points of such specification, and can be bound with different components depending on later design decisions. Similarly, an adaptive system with multiple variation points may be represented as an incomplete specification, in which variability is replaced with appropriate alternatives. We show the applicability of this approach in the context of Statecharts and Labeled Transition Systems and provide algorithms and tool support. Part III focuses on verification of stochastic software product lines (SPLs) for non-functional properties, namely reliability and energy consumption. We propose two modeling approaches to capturing stochastic behavior of SPLs. One approach enriches UML Sequence Diagrams with variability and stochastic information to represent high-level system scenarios. Second modeling, instead, extends Markov models with variability elements. Moreover, we propose three model-checking algorithms for the latter formalism, and discuss their performance and application. Finally we customize our framework to build model-based adaptive systems, which can continuously monitor, check, and satisfy non-functional requirements. In this case, we discuss the application of Dynamic SPLs.

L’OBIETTIVO di questa tesi è sviluppare tecniche per verificare diver- se proprietà dei Variability-Intensive Systems. La prima parte si occupa con gli definizioni base che serve per segui- re altre due parti. Con Variability-Intensive Systems, ci riferiamo ad una specifica dalla quale i vari sistemi possono essere derivate. Adaptive Sy- stems e Software Product Lines (SPL) sono due importanti esempi di tali sistemi. Nel primo caso, il sistema cambia tra diverse configurazioni in fa- se di esecuzione. Nel secondo caso ogni configurazione valida è rilasciato e come un singolo prodotto in fase di sviluppo. Specifiche incomplete di comportamento del sistema, che sono progressivamente sviluppate durante lo sviluppo, sono un altro tipo di specifiche che si evolvono nel tempo, e possono portare a versioni differenti. Classifichiamo la variabilità in due classi: aperta e chiusa. Di conseguenza, la tesi è divisa in due parti prin- cipali, che sono dedicati a questi due tipi di sistemi. La variabilità aperta riguarda i casi in cui le specifiche di altre alternative sono sconosciute, che è il caso di specifiche incompleti. Questo è esattamente opposta in caso delle SPL che la variabilità è chiusa e la specifica è completa. La seconda parte presenta un nuovo approccio per la specifica e la veri- fica di modelli di software incompleti rispetto le proprietà logiche tempo- rali e particolarmente CTL. Un modello incompleto può rappresentare un disegno parziale di un sistema nelle prime fasi del sviluppo, in cui alcu- ni componenti non sono ancora stati specificati. I componenti sconosciuti possono essere visti come punti di variazione di tale specifica, e possono essere associati con diversi componenti a seconda delle decisioni di pro- gettazione successivi. Analogamente, un sistema adattivo con più punti di variazione può essere rappresentato come una specifica incompleta, in cui la variabilità è sostituita con alternative appropriate. Mostriamo l’applicabi- lità di questo approccio nel contesto dagli Statecharts e Labeled Transition Systems e forniamo algoritmi e strumenti di supporto. La terza parte si concentra sulla verifica delle linee di prodotti software stocastico per requisiti non-funzionali, vale a dire affidabilita e il consumo di energia. Proponiamo due approcci di modellazione per rappresentare il comportamento stocastico di SPL. Il nostro approccio arricchisce dia- grammi di sequenza UML con punti di variabilità e informazioni stocastici a rappresentare scenari di sistemi di alto livello. Inoltre la modellazione estende i modelli di Markov con elementi di variabilità. Inoltre, propo- niamo tre algoritmi di controllo per quest’ultimo formalismo, e discutiamo le loro prestazioni e applicazioni. Infine abbiamo personalizzato il nostro framework per costruire Adaptive Systems basati su modelli, che possono monitorare, controllare e soddisfare i requisiti non-funzionali. In questo caso, si discute l’applicazione della dinamica alla SPL.