Variability Management of Reliability Models in Software Product Lines: An Expressiveness and Scalability Analysis

Some domains, specially those of critical systems, require dependable software. Ensuring dependability is not a trivial problem. Model checking can be used to estimate the reliability of a software through models that represent the behavior of the system. Through these models it is possible to estimate and measure quantitatively properties such as reliability. In the context of Software Product Lines (SPL), we need to check an entire family of systems. It is not feasible to build a model for each configuration of a SPL as the number of models required can be very large. Some contributions directly address this issue proposing techniques specifically tailored for SPL. Particularly, the technique of parametric model-checking allows the use of a single model to obtain properties values from different configurations through an arithmetic formula. However, even an arithmetic formula may not be easy to evaluate. If the number of operands is large enough the cost of evaluation of this formula could also be large. Current techniques may impose limitations over the variability and/or system architecture. To the best of our knowledge, to handle variability on model checking is still an open problem. This work is an investigation of the whole process of obtaining a parametric arithmetic formula for a SPL. Knowing this process and the factors that directly affect the growth of the formula, we are able to develop new techniques to deal with parametric model-checking in SPL with less restrictions.