Systematic Derivation of Static Analyses for Software Product Lines

TR-2014-170, Authors: Jan Midtgaard, Claus Brabrand & Andrzej Wasowski.

Systematic Derivation of Static Analyses for Software Product Lines

Jan Midtgaard

Claus Brabrand

Andrzej Wasowski

March 2014

Abstract

A recent line of work lifts particular verification and analysis methods to Software Product Lines (SPL). In an effort to generalize such case-by-case approaches, we develop a systematic methodology for lifting program analyses to SPLs using abstract interpretation. Abstract interpretation is a classical framework for deriving static analyses in a compositional, step-by-step manner. We show how to take an analysis expressed as an abstract interpretation and lift each of the abstract interpretation steps to a family of programs. This includes schemes for lifting domain types, and combinators for lifting analyses and Galois connections. We prove that for analyses developed using our method, the soundness of lifting follows by construction. Finally, we discuss approximating variability in an analysis and we derive variational data-flow equations for an example analysis, a constant propagation analysis for a simple imperative language.

Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.2 [Theory of Computation]: Semantics of Programming Languages —Program Analysis

General Terms Languages, Theory, Verification

Keywords Software Product Lines, Verification, Static Analysis, Abstract Interpretation

Technical report TR-2014-170 in IT University Technical Report Series, March 2014. 

Available as PDF.