FLAME: FAMA Formal Framework (v 1.0): Technical Report ISA–12–TR–02

Abstract

Software product lines are rapidly gaining importance across different application domains. This software production paradigm focuses on the development of related software products using managed reusable assets instead of building each product from scratch. In the software product line community, feature models are recognized as one of the most used notation to represent variability in a product line and their automated analysis is a thriving research area. In a recent systematic literature review, some of the authors summarized the numerous contributions on the topic in the last 20 years and identified several challenges to be addressed. One of them was the lack of formal definitions of the analysis operations, for which most of the reviewed works only provided informal descriptions, leading to misunderstandings and implementation problems in tool development. To face this challenge, this article presents FLAME, a formal framework for the specification of analysis operations on feature models. Its main advantages lie in its formal semantics—described using the Z specification language—and in its high level of abstraction, which allows the reuse of the framework for the formalization of different feature model dialects or even for different variability notations. Furthermore, in order to assure the quality of the formal framework—and to provide a reference implementation for tool developers—, the Z specification has been animated in Prolog and automatically validated using 18,000 test cases automatically generated using metamorphic testing techniques. The results of the performed tests have helped not only to enhance the framework significantly but also to detect inconsistencies both in the previous informal definitions of the analysis operations and in current analysis tools, thus supporting the need for formal semantics.