Beyond Boolean product-line model checking: Dealing with feature attributes and multi-features

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

84 Downloads (Pure)

Abstract

Model checking techniques for software product lines (SPL) are actively researched. A major limitation they currently have is the inability to deal efficiently with non-Boolean features and multi-features. An example of a non-Boolean feature is a numeric attribute such as maximum number of users which can take different numeric values across the range of SPL products. Multi-features are features that can appear several times in the same product, such as processing units which number is variable from one product to another and which can be configured independently. Both constructs are extensively used in practice but currently not supported by existing SPL model checking techniques. To overcome this limitation, we formally define a language that integrates these constructs with SPL behavioural specifications. We generalize SPL model checking algorithms correspondingly and evaluate their applicability. Our results show that the algorithms remain efficient despite the generalization.

Original languageEnglish
Title of host publicationProceedings - International Conference on Software Engineering
Pages472-481
Number of pages10
DOIs
Publication statusPublished - 30 Oct 2013
Event2013 35th International Conference on Software Engineering, ICSE 2013 - San Francisco, United States
Duration: 18 May 201326 May 2013

Conference

Conference2013 35th International Conference on Software Engineering, ICSE 2013
CountryUnited States
CitySan Francisco
Period18/05/1326/05/13

Keywords

  • Feature Cardinalities
  • Model Checking
  • Numeric Features
  • Semantics
  • Software Product Lines
  • Tools

Fingerprint Dive into the research topics of 'Beyond Boolean product-line model checking: Dealing with feature attributes and multi-features'. Together they form a unique fingerprint.

Cite this