Lightweight Methods for Effective Verification of Software Product Lines with Off-the-Shelf Tools

Certification is the process of assessing the quality of a product and whether it meets a set of requirements and adheres to functional and safety standards. I is often legally required to provide guarantee for human safety and to make the product available on the market. The certification process relies on objective evidence of quality, which is produced by using qualified and state-of-the-art tools and verification and validation techniques.
Software product line (SPL) engineering distributes costs among similar products that are developed simultaneously. However, SPL certification faces major challenges, partly due to the lack of qualified, state-of-the-art tools to support the development process in the presence of variability. In practice, there are cases in which it is too costly or complicated to qualify the support tools; in other cases state-of-the-art tools exist, but do not handle variability.
In this thesis, I identify three key challenges to SPL certification. I address them by proposing effective, lightweight methods that employ off-the-shelf tools for supporting and verifying SPL development. All the proposed methods are generalizable to a large part of existing tools, they are formally specified and accompanied by proof-of-concept implementations.
The first challenge is that of qualifying variant derivation tools. Any error that occurs in the process of deriving/building products from an SPL can affect the quality of the products themselves. Qualifying variant derivation tools requires a formal specification, which lacks or is incomplete for most variability modeling languages. I propose a lightweight verification technique based on translation validation, which uses formal specification written in a core variability modeling language.
The second challenge is that of validating SPL reengineering projects that involve complex source code transformations. To facilitate product (re)certification, the transformation must preserve certain qualitative properties such as code structure and semantics—a difficult task due to the complexity of the transformation and because certain properties, such as semantic equivalence, are generally difficult to verify. I present a number of lessons learned from a code modernization project involving a non-trivial rewriting transformation and a validation phase, which identifies and analyzes a number of transformation bugs that could not be detected with regular unit testing.
The third challenge is that of using state-of-the-art analysis tools to verify product families. Most off-the-shelf tools cannot handle variability in SPLs. Alternatively we can either verify each product individually (brute force) or develop lifted analysis tools that can handle variability, both approaches being costly and time-consuming. I investigate the possibility of using off-the-shelf analysis tools by rewriting compile-time variability into run-time variability.