Search

The model-checking problem for software product lines is harder than for single systems. Indeed, one has to verify all the software variants of a product line, whose number grows exponentially in the number of their differences. Techniques intended for single systems are inefficient in this case, for these can only be applied to all products separately. Variability-aware modelling formalisms and algorithms were designed as a more appropriate answer to that problem. Their strength lies in their ability to check a behaviour common to several products only once, which leads to substantial performance gains. Although they constitute a major step toward the efficient verification of product lines, these techniques are not yet mature enough to truly achieve this objective. They still lack optimisations to verify large models, the expressiveness to represent complex forms of variable behaviour, as well as usable languages and tools required for industrial transfer. This thesis aims at improving product-line model checking in order to provide formalisms, algorithms, and tools that together hold the potential to verify real-world software product lines. We first study the state-of-the-art model-checking approaches for software product lines. We compare them in terms of available formalisms and algorithms, and we determine that the approach based on Featured Transition Systems (FTS) is the most suitable to act as a basis for the design of novel techniques. We then extend its theory along two axes: efficiency and expressiveness. For the former, we propose abstraction methods that can reduce the size of the model to check while maintaining correctness and completeness; they consist of extensions of single-system abstraction techniques applied to FTS, and of new techniques that abstract away from their variability. As for expressiveness, on the one hand we propose featured timed automata as a combination of FTS and real-time behaviour. On the other hand, we analyse how to suppor, (DOCSC06) -- UNamur, 2014

The feature-interaction problem is a major threat to modularity and impairs compositional development and reasoning. A feature interaction occurs when the behavior of one feature is affected by the presence of another feature; often it cannot be deduced easily from the behaviors of the individual features involved. The feature-interaction problem became a crisis in the telecommunications industry in the late 1980s, and researchers responded with formalisms that enable automatic detection of feature interactions, architectures that avoid classes of interactions, and techniques for resolving interactions at run-time. While this pioneering work was foundational and very successful, it is limited in the sense that it is based on assumptions that hold only for telecommunication systems. In the meantime, different notions of feature interactions have emerged in different communities, including Internet applications, service systems, adaptive systems, automotive systems, software product lines, requirements engineering, and computational biology. So, feature interactions are a much more general concept than investigated in the past in the context of telecommunication systems, but a classification, comparison, and generalization of the multitude of different views is missing. The feature-interaction problem is still of pivotal importance in various industrial applications, and the Dagstuhl seminar "Feature Interactions: The Next Generation" gathered researchers and practitioners from different areas of computer science and other disciplines with the goal to compare, discuss, and consolidate their views, experience, and domain-specific solutions to the feature-interaction problem.

Polylith is a software interconnection system that allows programmers to configure applications from mixed-language software components (modules), and then execute those applications in diverse environments. In general, communication between components can be implemented with TCP/IP or XNS protocols in a network; via shared memory between light-weight threads on a tightly coupled multiprocessor; using custom-hardware channels between processors; or using simply a 'branch' instruction within the same process space. Flexibility in how components are interconnected is made possible by a 'software bus' organization. This document serves as a manual for programmers who wish to use one particular software busthe TCP/IP-based network bus. (Also cross-referenced as UMIACS-TR-90-149)

Precise notations have been developed to specify unambiguous requirements and ensure that all cases of appropriate system behavior are considered and documented. Using one such notation, we have developed techniques to automatically analyze software artifacts at early stages of the software development life cycle. We use model checking as our verification technique because it can be fully automated and can check properties of large systems. This report describes model checking and summarizes our efforts to use it to analyze software requirements and designs. We prove that requirements model system safety properties and that designs model consistency properties derived from requirements by creating abstractions of these software artifacts and using model checking to determine if the abstractions are models of the properties. We present results from a case study in which we analyzed the requirements and design of a small but realistic system.