@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 = {https://publikationen.bibliothek.kit.edu/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.} }
Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof Reuse
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: | https://publikationen.bibliothek.kit.edu/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.