1,720,964 research outputs found
Model-Based Verification of Quantitative Non-Functional Properties for Software Product Lines
No full textEvaluating quality attributes of a design model in the early stages of development can significantly reduce the cost and risks of developing a low quality product. To make this possible, software designers should be able to predict quality attributes by reasoning on a model of the system under development. Although there exists a variety of quality-driven analysis techniques for software systems, only a few work address software product lines. This paper describes how probabilistic model checking techniques and tools can be used to verify non-functional properties of different configurations of a software product line. We propose a model-based approach that enables software engineers to assess their design solutions for software product lines in the early stages of development. Furthermore, we discuss how the analysis time can be surprisingly reduced by applying parametric model checking instead of classic model checking. The results show that the parametric approach is able to substantially alleviate the verification time and effort required to analyze non-functional properties of software product lines
LOVER: Light-weight fOrmal Verification of adaptivE systems at Run time
No full textAdaptive systems are able to modify their behaviors to re-
spond to signicant changes at run time such as component failures. In many cases, run-time adaptation is simply replacing a piece of system with a new one without interrupting the system operation. In terms of component-based systems, an adaptation may be dened as replacing a system component with a new version at run time. However, updating a system with new components requires the assurance that the new conguration will fully satisfy the expected requirements. Formal verication has been widely used to guarantee that a system specication satises a set of properties. However, applying verication techniques at run time for any potential change can be very expensive and sometimes unfeasible. In this paper, we present a framework, called LOVER, for the lightweight verication of component-based adaptive systems at run time. LOVER provides a new process model supported with formalisms, verication algorithms and tool to verify a signicant subset of CTL properties
On requirement verification for evolving Statecharts specifications
No full textSoftware development processes have been evolving from rigid, pre-specified, and sequential to incremental, and iterative. This evolution has been dictated by the need to accommodate evolving user requirements and reduce the delay between design decision and feedback from users. Formal verification techniques, however, have largely ignored this evolution and even when they made enormous improvements and found significant uses in practice, like in the case of model checking, they remained confined into the niches of safety-critical systems. Model checking verifies if a system's model M satisfies a set of requirements, formalized as a set of logic properties Φ. Current model-checking approaches, however, implicitly rely on the assumption that both the complete model M and the whole set of properties Φ are fully specified when verification takes place. Very often, however, M is subject to change because its development is iterative and its definition evolves through stages of incompleteness, where alternative design decisions are explored, typically to evaluate some quality trade-offs. Evolving systems specifications of this kind ask for novel verification approaches that tolerate incompleteness and support incremental analysis of alternative designs for certain functionalities. This is exactly the focus of this paper, which develops an incremental model-checking approach for evolving Statecharts. Statecharts have been chosen both because they are increasingly used in practice natively support model refinements
Requirements Verification of Variability-Intensive Systems
Get PDFL’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.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.DIPARTIMENTO DI ELETTRONICA, INFORMAZIONE E BIOINGEGNERIA25CUGOLA, GIANPAOLOFIORINI, CARLO ETTOR
Features meet scenarios:Modeling and consistency-checking scenario-based product line specifications
No full textMany modern software-intensive systems consist of multiple components interacting together to deliver the intended functionality. Often, these systems come in many variants (products) and are managed together as a software product line. This variability is the source of additional complexity which can cause inconsistencies and offset the economies of scale promised by product line engineering. Engineers thus need intuitive, yet precise means for specifying requirements and require tools for automatically detecting inconsistencies within these requirements. In recent work, we proposed a technique for the scenario-based specification of interactions in product lines by a combination of Modal Sequence Diagrams and Feature Diagrams. Furthermore, we elaborated an efficient consistency-checking technique based on a dedicated model-checking approach especially tailored for product lines. In this paper, we report on further evaluations that underline significant performance benefits of our approach. We describe further optimizations and detail on how we encode the consistency-checking problem for a model-checker.</p
Efficient Consistency Checking of Scenario-Based Product Line Specifications [Best paper award]
Get PDF
- …
