Paper Info
Title
FLAME: a formal framework for the automated analysis of software product lines validated by automated specification testing
Abstract
Abstract In a literature review on the last 20 years of automated analysis of feature models, the formalization of analysis operations was identified as the most relevant challenge in the field. This formalization could provide very valuable assets for tool developers such as a precise definition of the analysis operations and, what is more, a reference implementation, i.e., a trustworthy, not necessarily efficient implementation to compare different tools outputs. In this article, we present the FLAME framework as the result of facing this challenge. FLAME is a formal framework that can be used to formally specify not only feature models, but other variability modeling languages (VML s) as well. This reusability is achieved by its two-layered architecture. The abstract foundation layer is the bottom layer in which all VML-independent analysis operations and concepts are specified. On top of the foundation layer, a family of characteristic model layers—one for each VML to be formally specified—can be developed by redefining some abstract types and relations. The verification and validation of FLAME has followed a process in which formal verification has been performed traditionally by manual theorem proving, but validation has been performed by integrating our experience on metamorphic testing of variability analysis tools, something that has shown to be much more effective than manually designed test cases. To follow this automated, test-based validation approach, the specification of FLAME, written in Z, was translated into Prolog and 20,000 random tests were automatically generated and executed. Tests results helped to discover some inconsistencies not only in the formal specification, but also in the previous informal definitions of the analysis operations and in current analysis tools. After this process, the Prolog implementation of FLAME is being used as a reference implementation for some tool developers, some analysis operations have been formally specified for the first time with more generic semantics, and more VML s are being formally specified using FLAME.
Year
DOI
Venue
2017
10.1007/s10270-015-0503-z
Software and Systems Modeling
Keywords
Field
DocType
Formal specification,Specification testing,Software product lines,Feature models
Programming language,Systems engineering,Software engineering,Verification and validation,Computer science,Automated theorem proving,Modeling language,Formal specification,Reference implementation,Metamorphic testing,Test case,Formal verification
Journal
Volume
Issue
ISSN
16
4
1619-1374
Citations 
PageRank 
References 
6
0.43
48
Authors
5
Name
Order
Citations
PageRank
Amador Durán111414.59
David Benavides243630.52
Sergio Segura3129554.49
Pablo Trinidad444423.01
Antonio Ruiz Cortés584766.93