Towards Cost-Effective High-Assurance Software Product Lines: The Need for Property-Preserving Transformations

Generative programming and model transformation techniques are becoming widely used for the development of software components for product lines. The ability to develop components with identified common and variable parts, and rapidly instantiate product-specific versions is key to many software product line approaches. However if this approach is to be truly cost effective for high assurance applications, the instantiation process must be property-preserving, any verification evidence acquired on the product-line component must be demonstrably applicable to the instantiated component. In this paper we outline an approach that uses static analysis techniques and the SPARK language that can potentially demonstrate the correctness of model transformations.