Requirements Verification of Variability-Intensive Systems
Amir Molzam Sharifloo · 2014
L’OBIETTIVO di questa tesi e sviluppare tecniche per verificare diver- se proprieta 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 e 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 variabilita in due classi: aperta e chiusa. Di conseguenza, la tesi e divisa in due parti prin- cipali, che sono dedicati a questi due tipi di sistemi. La variabilita aperta riguarda i casi in cui le specifiche di altre alternative sono sconosciute, che e il caso di specifiche incompleti. Questo e esattamente opposta in caso delle SPL che la variabilita e chiusa e la specifica e completa. La seconda parte presenta un nuovo approccio per la specifica e la veri- fica di modelli di software incompleti rispetto le proprieta logiche tempo- rali e particolarmente CTL. Un modello incompleto puo 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 piu punti di variazione puo essere rappresentato come una specifica incompleta, in cui la variabilita e sostituita con alternative appropriate. Mostriamo l’applicabi- lita 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 variabilita e informazioni stocastici a rappresentare scenari di sistemi di alto livello. Inoltre la modellazione estende i modelli di Markov con elementi di variabilita. 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.