Theorem proving for product line model verification

Mike Mannion*, Javier Camara

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

24 Citations (Scopus)


Product line models of requirements can be used to drive the selection of requirements of new systems in the product line. Validating any selected single system is difficult because product line models are large and complex. However by modelling variability and dependency between requirements using propositional connectives a logical expression can be developed for the model and then selection validation can be achieved by satisfying the logical expression. This approach can be used to validate the model as a whole. A case study with nearly 800 requirements is presented and the computational aspects of the approach are discussed.
Original languageEnglish
Title of host publicationSoftware Product-Family Engineering: 5th International Workshop, PFE 2003, Siena, Italy, November 4-6, 2003, Revised Papers
EditorsFrank van der Linden
Place of PublicationBerlin
PublisherSpringer Nature
Number of pages14
ISBN (Electronic)9783540246671
ISBN (Print)9783540219415
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


  • mobile phone
  • theorem prove
  • single system
  • software product line
  • logical expression


Dive into the research topics of 'Theorem proving for product line model verification'. Together they form a unique fingerprint.

Cite this