Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof Reuse

Technical Report

Author(s):Daniel Bruns, Vladimir Klebanov, and Ina Schaefer
Booktitle:Papers Presented at the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
Institution:Department of Informatics, Karlsruhe Institute of Technology
Series:Karlsruhe Reports in Informatics
Number:2010-13
Year:2010
Pages:345-358
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019096

Abstract

Software product lines (SPL) are a well-known methodology to develop industry-size adaptable software systems. SPL are often used in domains where high-quality software is desirable, but the overwhelming product diversity remains a challenge for assuring correctness. We present our work in progress on reducing the deductive verification effort across different products of an SPL. On the specification side, our approach enriches the delta language for describing SPLs with formal product specifications. On the verification side, we combine program slicing and similarity-guided proof reuse to ease the verification process.

BibTeX

@TechReport{BrunsKlebanovSchaefer10,
  author	= {Daniel Bruns and Vladimir Klebanov and Ina Schaefer},
  title		= {Verification of Software Product Lines: Reducing the
		   Effort with Delta-oriented Slicing and Proof Reuse},
  year		= 2010,
  month		= jun,
  address	= {Paris, France},
  booktitle	= {Papers Presented at the International Conference on Formal
		   Verification of Object-Oriented Software ({FoVeOOS} 2010)},
  editor	= {Bernhard Beckert and Claude March{\'e}},
  language	= {english},
  institution	= {Department of Informatics, Karlsruhe
		   Institute of Technology},
  series	= {Karlsruhe Reports in Informatics},
  number	= {2010-13},
  url		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019096},
  urn		= {urn:nbn:de:swb:90-190964},
  pages		= {345--358},
  abstract	= {Software product lines (SPL) are a well-known methodology
		   to develop industry-size adaptable software systems. SPL
		   are often used in domains where high-quality software is
		   desirable, but the overwhelming product diversity remains a
		   challenge for assuring correctness. We present our work in
		   progress on reducing the deductive verification effort
		   across different products of an SPL. On the specification
		   side, our approach enriches the delta language for
		   describing SPLs with formal product specifications. On the
		   verification side, we combine program slicing and
		   similarity-guided proof reuse to ease the verification
		   process.}
}