Compositional type checking of delta-oriented software product lines

Delta-oriented programming is a compositional approach to flexibly implementing software product lines. A product line is represented by a code base and a product line declaration. The code base consists of a set of delta modules specifying modifications to object-oriented programs. A particular product in a delta-oriented product line is generated by applying the modifications contained in the suitable delta modules to the empty program. The product-line declaration provides the connection of the delta modules with the product features. This separation increases the reusability of delta modules. In this paper, we provide a foundation for compositional type checking of delta-oriented product lines of Java programs by presenting a minimal core calculus for delta-oriented programming. The calculus is equipped with a constraint-based type system that allows analyzing each delta module in isolation, such that the results of the analysis can be reused. By relying only on the analysis results for the delta modules and on the product line declaration, it is possible to establish whether all the products of the product line are well typed according to the fragment of the Java type system modeled by the calculus.     

Model checking software product lines with SNIP

We present SNIP, an efficient model checker for software product lines (SPLs). Variability in software product lines is generally expressed in terms of features, and the number of potential products is exponential in the number of features. Whereas classical model checkers are only capable of checking properties against each individual product in the product line, SNIP exploits specifically designed algorithms to check all products in a single step. This is done by using a concise mathematical structure for product line behaviour, that exploits similarities and represents the behaviour of all products in a compact manner. Specification of an SPL in SNIP relies on the combination of two specification languages: TVL to describe the variability in the product line, and fPromela to describe the behaviour of the individual products. SNIP is thus one of the first tools equipped with specification languages to formally express both the variability and the behaviours of the products of the product line. The paper assesses SNIP and suggests that this is the first model checker for SPLs that can be used outside the academic arena.     

Compositional encoding for bounded model checking

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit onthe-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.     

Evolving feature model configurations in software product lines

The increasing complexity and cost of software-intensive systems has led developers to seek ways of reusing software components across development projects. One approach to increasing software reusability is to develop a software product-line (SPL), which is a software architecture that can be reconfigured and reused across projects. Rather than developing software from scratch for a new project, a new configuration of the SPL is produced. It is hard, however, to find a configuration of an SPL that meets an arbitrary requirement set and does not violate any configuration constraints in the SPL.Existing research has focused on techniques that produce a configuration of an SPL in a single step. Budgetary constraints or other restrictions, however, may require multi-step configuration processes. For example, an aircraft manufacturer may want to produce a series of configurations of a plane over a span of years without exceeding a yearly budget to add features.This paper provides three contributions to the study of multi-step configuration for SPLs. First, we present a formal model of multi-step SPL configuration and map this model to constraint satisfaction problems (CSPs). Second, we show how solutions to these SPL configuration problems can be automatically derived with a constraint solver by mapping them to CSPs. Moreover, we show how feature model changes can be mapped to our approach in a multi-step scenario by using feature model drift. Third, we present empirical results demonstrating that our CSP-based reasoning technique can scale to SPL models with hundreds of features and multiple configuration steps.     

Retrieving reusable components with variation points from software product lines

Reusing software through software product lines has been recognized as useful. To improve reuse efficiency, retrieving proper systems or subsystems from software product lines for reuse is an important issue. This paper proposes a technique to retrieve reusable software systems/subsystems from software product lines.     

Modeling software product lines using color-blind transition systems

Families of embedded discrete finite state programs are modeled using input-enabled alternating transition systems. One model describes all functionality, while each variant is defined by an environment, describing its possible uses. The environments show both the inputs that a system can receive and indicate which of the system’s responses are relevant for the environment. The latter trait, called color-blindness, creates new possibilities for system transformations in the specialization process. We demonstrate the use of the framework by applying it to two classes of realistic design languages. An example of a product line of alarm clocks is used throughout the article.     

IC3 software model checking

International Journal on Software Tools for Technology Transfer - In recent years, the inductive, incremental verification algorithm IC3 had a major impact on hardware model checking. Also for...     

Checking JML specifications using an extensible software model checking framework

The use of assertions to express correctness properties of programs is growing in practice. Assertions provide a form of lightweight checkable specification that can be very effective in finding defects in programs and in guiding developers to the cause of a problem. A wide variety of assertion languages and associated validation techniques have been developed, but run-time monitoring is commonly thought to be the only practical solution. In this paper, we describe how specifications written in the Java Modeling Language (JML), a general purpose behavioral specification and assertional language for Java, can be validated using a customized model checker built on top of the Bogor model checking framework. Our experience illustrates the need for customized state-space representations and reduction strategies in model checking frameworks in order to effectively check the kind of strong behavioral specifications that can be written in JML. We discuss the advantages and tradeoffs of model checking relative to other specification validation techniques and present data that suggest that the cost of model checking strong specifications is practical for several real programs. This is an extended version of the paper Checking Strong Specifications Using An Extensible Model Checking Framework that appeared in Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004. This work was supported in part by the U.S. Army Research Office (DAAD190110564), by DARPA/IXO’s PCES program (AFRL Contract F33615-00-C-3044), by NSF (CCR-0306607) by Lockheed Martin, and by Rockwell-Collins.     

Compositional checking of satisfaction

We present a compositional method for deciding whether a process satisfies an assertion. Assertions are formulas in a modal -calculus, and processes are drawn from a very general process algebra inspired by CCS and CSP. Well-known operators from CCS, CSP, and other process algebras appear as derived operators. The method iscompositional in the structure of processes and works purely on the syntax of processes. It consists of applying a sequence ofreductions, each of which only takes into account the top-level operator of the process. A reduction transforms a satisfaction problem for a composite process into equivalent satisfaction problems for the immediate subcomponents. Using process variables, systems with underfined subcomponents can be defined, and given an overall requirement to the system,necessary and sufficient conditions on these subcomponents can be found. Hence the process variables make it possible to specify and reason about what are often referred to ascontexts, environments, andpartial implementations. Since reductions are algorithms that work on syntax, they can be considered as forming a bridge between traditional noncompositional model checking and compositional proof systems.     

Efficient software product-line model checking using induction and a SAT solver

Software product line (SPL) engineering is increasingly being adopted in safety-critical systems. It is highly desirable to rigorously show that these systems are designed correctly. However, formal analysis for SPLs is more difficult than for single systems because an SPL may contain a large number of individual systems. In this paper, we propose an efficient model-checking technique for SPLs using induction and a SAT (Boolean satisfiability problem) solver. We show how an induction-based verification method can be adapted to the SPLs, with the help of a SAT solver. To combat the state space explosion problem, a novel technique that exploits the distinguishing characteristics of SPLs, called feature cube enlargement, is proposed to reduce the verification efforts. The incremental SAT mechanism is applied to further improve the efficiency. The correctness of our technique is proved. Experimental results show dramatic improvement of our technique over the existing binary decision diagram (BDD)-based techniques.     

Calculating ROI for software product lines

Product line engineering has become an important and widely used approach for efficiently developing portfolios of software products. The idea is to develop a set of products as a single, coherent development task from a core asset base (sometimes called a platform), a collection of artifacts specifically designed for use across a portfolio. This approach produces order-of-magnitude economic improvements compared to one-at-a-time software system development. Because the product line approach isn't limited to specific technical properties of the planned software but rather focuses on economic characteristics, high return on investment has become the anthem of the approach's protagonists. Our software product line cost model can calculate the costs and benefits (and hence the ROI) that we can expect to accrue from various product line development situations. It's also straightforward and intuitive.     

Bounded model checking of software using SMT solvers instead of SAT solvers

C bounded model checking (cbmc) has proved to be a successful approach to automatic software analysis. The key idea is to (i) build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property and (ii) use state-of-the-art SAT solvers to check the resulting formulae for satisfiability. In this paper, we propose a generalisation of the cbmc approach on the basis of an encoding into richer (but still decidable) theories than propositional logic. We show that our approach may lead to considerably more compact formulae than those obtained with cbmc. We have built a prototype implementation of our technique that uses a satisfiability modulo theories (SMT) solver to solve the resulting formulae. Computer experiments indicate that our approach compares favourably with—and on some significant problems outperforms—cbmc.     

Key activities for product derivation in software product lines

More and more organizations adopt software product lines to leverage extensive reuse and deliver a multitude of benefits such as increased quality and productivity and a decrease in cost and time-to-market of their software development. When compared to the vast amount of research on developing product lines, relatively little work has been dedicated to the actual use of product lines to derive individual products, i.e., the process of product derivation. Existing approaches to product derivation have been developed independently for different aims and purposes. While the definition of a general approach applicable to every domain may not be possible, it would be interesting for researchers and practitioners to know which activities are common in existing approaches, i.e., what are the key activities in product derivation. In this paper we report on how we compared two product derivation approaches developed by the authors in two different, independent research projects. Both approaches independently sought to identify product derivation activities, one through a process reference model and the other through a tool-supported derivation approach. Both approaches have been developed and validated in research industry collaborations with different companies. Through the comparison of the approaches we identify key product derivation activities. We illustrate the activities’ importance with examples from industry collaborations. To further validate the activities, we analyze three existing product derivation approaches for their support for these activities. The validation provides evidence that the identified activities are relevant to product derivation and we thus conclude that they should be considered (e.g., as a checklist) when developing or evaluating a product derivation approach.     

Exemplar driven development of software product lines

The benefits of following a product line approach to develop similar software systems are well documented. Nevertheless, some case studies have revealed significant barriers to adopt such approach. In order to minimize the paradigm shift between conventional software engineering and software product line engineering, this paper presents a new development process where the products of a domain are made by analogy to an existing product. Furthermore, this paper discusses the capabilities and limitations of different techniques to implement the analogy relation and proposes a new language to overcome such limitations.     

Automatic software model checking via constraint logic

This paper proposes the use of constraint logic to perform model checking of imperative, infinite-state programs. We present a semantics-preserving translation from an imperative language with recursive procedures and heap-allocated mutable data structures into constraint logic. The constraint logic formulation provides a clean way to reason about the behavior and correctness of the original program. In addition, it enables the use of existing constraint logic implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration.     

A formal framework for software product lines

ContextA Software Product Line is a set of software systems that are built from a common set of features. These systems are developed in a prescribed way and they can be adapted to fit the needs of customers. Feature models specify the properties of the systems that are meaningful to customers. A semantics that models the feature level has the potential to support the automatic analysis of entire software product lines.ObjectiveThe objective of this paper is to define a formal framework for Software Product Lines. This framework needs to be general enough to provide a formal semantics for existing frameworks like FODA (Feature Oriented Domain Analysis), but also to be easily adaptable to new problems.MethodWe define an algebraic language, called SPLA, to describe Software Product Lines. We provide the semantics for the algebra in three different ways. The approach followed to give the semantics is inspired by the semantics of process algebras. First we define an operational semantics, next a denotational semantics, and finally an axiomatic semantics. We also have defined a representation of the algebra into propositional logic.ResultsWe prove that the three semantics are equivalent. We also show how FODA diagrams can be automatically translated into SPLA. Furthermore, we have developed our tool, called AT, that implements the formal framework presented in this paper. This tool uses a SAT-solver to check the satisfiability of an SPL.ConclusionThis paper defines a general formal framework for software product lines. We have defined three different semantics that are equivalent; this means that depending on the context we can choose the most convenient approach: operational, denotational or axiomatic. The framework is flexible enough because it is closely related to process algebras. Process algebras are a well-known paradigm for which many extensions have been defined.     

Flexible feature binding in software product lines

A software product line (SPL) is a family of programs that share assets from a common code base. The programs of an SPL can be distinguished in terms of features, which represent units of program functionality that satisfy stakeholders’ requirements. The features of an SPL can be bound either statically at program compile time or dynamically at run time. Both binding times are used in SPL development and have different advantages. For example, dynamic binding provides high flexibility whereas static binding supports fine-grained customizability without any impact on performance (e.g., for use on embedded systems). However, contemporary techniques for implementing SPLs force a programmer to choose the binding time already when designing an SPL and to mix different implementation techniques when multiple binding times are needed. We present an approach that integrates static and dynamic feature binding seamlessly. It allows a programmer to implement an SPL once and to decide per feature at deployment time whether it should be bound statically or dynamically. Dynamic binding usually introduces an overhead regarding resource consumption and performance. We reduce this overhead by statically merging features that are used together into dynamic binding units. A program can be configured at run time by composing binding units on demand. We use feature models to ensure that only valid feature combinations can be selected at compile and at run time. We provide a compiler and evaluate our approach on the basis of two non-trivial SPLs.     

Extracting core requirements for software product lines

Requirements Engineering - Software Product Line Engineering (SPLE) is a promising paradigm for reusing knowledge and artifacts among similar software products. However, SPLE methods and techniques...