Please use this identifier to cite or link to this item:
Title: Formal semantics and verification for feature modeling
Authors: Sun, J.
Zhang, H.
Li, Y.F. 
Wang, H.
Keywords: Alloy
Domain Engineering
Feature Modeling
Feature Oriented Domain Analysis
Formal Verification
Issue Date: 2005
Citation: Sun, J.,Zhang, H.,Li, Y.F.,Wang, H. (2005). Formal semantics and verification for feature modeling. Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS : 303-312. ScholarBank@NUS Repository.
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. © 2005 IEEE.
Source Title: Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

checked on Sep 22, 2022

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.