Synthesizing product line controllers from scenario based specifications

Modern software-intensive systems usually consist of a set of components which interact to achieve their functionalities. Often those systems are part of a family of product variants, also called Software Product Line (SPL). Variability in an SPL is commonly captured by features, i.e. functions or components that may or may not be present. Although reusing features leads to lower costs and shorter time in the SPL development process, it also adds complexity to the design task. In order to cope with that complexity, an intuitive, yet precise way to design those systems is required. Recent work proposes an SPL scenario-based specification where each feature is associated to a set of Modal Sequence Diagrams (MSD) specifying its behavioral aspects, allowing us to obtain the specification of a product by composing that of its constituent features. However inconsistencies may be introduced. If they remain undetected, some product could turn out to be unrealizable, leading to costly iterations in the later development. Thus it is important to ensure that each product is implementable, beforehand. This thesis presents a technique to automatically check the consistency of an SPL specification as a whole, instead of performing a separate check on each product. We exploit the fact that if variants are similar, the state graphs induced by each product's specification are also likely to be similar. Given an SPL specification we derive a global state graph representing all possible executions of all possible products in any environment. In such a graph we maintain a link between a given execution and the features needed to trigger it. This information is then used to determine which products are realizable. We evaluate the applicability and eficiency of our approach, achieving benefits over performing individual checking of each variant separately. We also compare our technique with an alternative incremental approach, optimized to be on-the-fly, i.e. exploring only parts of the state space. We discover that the latter still performs better when more of those graph portions can be avoided. We expect that remarkable results could be achieved by making our technique on-the-fly.

I sistemi software-intensive spesso consistono di un insieme di componenti che interagiscono per adempiere funzionalità complesse. Talvolta essi sono parte di una famiglia di prodotti simili, detta Software Product Line (SPL). Le differenze e le caratteristiche comuni tra ogni variante possono essere espresse da feature, cioè funzionalità o componenti facenti parte o meno del prodotto. Sebbene il riutilizzo di feature porti a una riduzione di costi e tempi nel processo di sviluppo di SPL, esso aggiunge maggiore complessità al design. Per far fronte a tale complessità, un recente lavoro propone una specifica SPL basata su scenari in cui, ad ogni feature, viene associato un insieme di Modal Sequence Diagram (MSD) che ne descrive il comportamento, permettendo di ottenere la specifica di un prodotto come combinazione delle specifiche delle feature che lo compongono. Tuttavia le eventuali inconsistenze nelle specifiche, se non tempestivamente rilevate, portano a costose iterazioni nella fase di sviluppo di prodotti non realizzabili. È dunque importante verificarne anticipatamente la consistenza. Questa tesi presenta una tecnica per la verifica automatica della consistenza di un'intera specifica SPL, alternativa all'esecuzione di verifiche individuali su ogni prodotto. Sfruttando il fatto che le specifiche di singole varianti generano state-graph simili, deriviamo uno state-graph globale da una specifica SPL, che rappresenta tutte le possibili esecuzioni per tutti i possibili prodotti. In questa fase viene mantenuto un legame tra un'esecuzione e le feature necessarie ad attivarla. Tali informazioni vengono successivamente utilizzate per determinare i prodotti realizzabili. Vengono valutate l'applicabilità e le prestazioni del nostro approccio, ottenendo vantaggi rispetto alla verifica consecutiva di ogni variante. In aggiunta ci confrontiamo con un approccio incrementale, ottimizzato per essere on-the-fly, ovvero per esplorare solo alcune parti dello state-graph. Scopriamo che quest'ultimo metodo risulta più effciente quando molte porzioni del grafo possono essere evitate. Riteniamo che notevoli risultati potrebbero essere raggiunti rendendo la nostra tecnica on-the-fly.