Verification of Software Product Lines with Delta-Oriented Slicing

Reviewed Paper In Proceedings

Author(s):Daniel Bruns, Vladimir Klebanov, and Ina Schaefer
In:Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:6528
Year:2010
Pages:61-75
URL:https://www.springerlink.com/content/441476732611n21t/
DOI:10.1007/978-3-642-18070-5_5

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

@InProceedings{BrunsKlebanovSchaefer2010,
  author        = {Daniel Bruns and
                   Vladimir Klebanov and
                   Ina Schaefer},
  title         = {Verification of Software Product Lines with Delta-Oriented
                   Slicing},
  year          = {2010},
  month         = jun,
  editor        = {Bernhard Beckert and
                   Claude March{\'e}},
  booktitle     = {Formal Verification of Object-Oriented Software
                   ({FoVeOOS} 2010), Revised Selected Papers},
  publisher     = {Springer},
  language      = {english},
  series        = {Lecture Notes in Computer Science},
  volume        = {6528},
  pages         = {61--75},
  isbn          = {978-3-642-18069-9},
  url           = {https://www.springerlink.com/content/441476732611n21t/},
  doi           = {10.1007/978-3-642-18070-5_5},
  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.}
}