|Thesis abstract: |
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.