Formal semantics and verification for feature modeling

Sun, J, Zhang, H, Li, Y and Wang, H 2005, 'Formal semantics and verification for feature modeling', in C. Ghezzi and Y. Fu (ed.) Proceedings of 10th IEEE International Conference on Engineering of Complex Computer Systems, Shanghai, 16-20 June 2005.


Document type: Conference Paper
Collection: Conference Papers

Title Formal semantics and verification for feature modeling
Author(s) Sun, J
Zhang, H
Li, Y
Wang, H
Year 2005
Conference name 10th IEEE International Conference on Engineering of Complex Computer Systems
Conference location Shanghai
Conference dates 16-20 June 2005
Proceedings title Proceedings of 10th IEEE International Conference on Engineering of Complex Computer Systems
Editor(s) C. Ghezzi
Y. Fu
Publisher IEEE
Place of publication Los Alamitos, CA
Abstract Research on features has received much attention in the domain engineering community. Feature modeling plays an important role in the design and implementation of complex software systems. However, the presentation and analysis of feature models are still largely informal. There is also an increasing need for methods and tools that can support automated feature model analysis. This paper presents a formal engineering approach to the specification and verification of feature models. A formal semantics for the feature modeling language is defined using first-order logic. It provides a precise and rigorous formal interpretation for the graphical notation. In addition, further validation of the semantics using the Z/EVES theorem prover is presented. Finally, we demonstrate that the consistency of a feature model and its configurations can be automatically verified by encoding the semantics into the Alloy Analyzer. A case study of the Key Word in Context (KWIC) index systems feature model is presented to illustrate the verification process.
Subjects Programming Languages
Keyword(s) feature modeling
domain engineering
feature oriented domain analysis
Z/EVES
alloy
formal verification
DOI - identifier 10.1109/ICECCS.2005.48
Copyright notice © 2005 IEEE
Versions
Version Filter Type
Altmetric details:
Access Statistics: 195 Abstract Views  -  Detailed Statistics
Created: Wed, 08 Apr 2009, 09:42:32 EST by Catalyst Administrator
© 2014 RMIT Research Repository • Powered by Fez SoftwareContact us