Towards Cost-Effective High-Assurance Software Product Lines: The Need for Property-Preserving Transformations
Software Product Line Conference, International (2011)
Aug. 22, 2011 to Aug. 26, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SPLC.2011.32
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.
UML, SPARK, M2M, Safety Critical, High Integrity, Software Product Lines, Verification, Static Analysis, DO-178B/ED-12B
J. McDermid and S. Hutchesson, "Towards Cost-Effective High-Assurance Software Product Lines: The Need for Property-Preserving Transformations," Software Product Line Conference, International(SPLC), Munich, Germany, 2011, pp. 55-64.