---
_id: '20891'
abstract:
- lang: eng
  text: "Today, software systems are rarely developed monolithically, but may be composed
    of numerous individually developed features. Their modularization facilitates
    independent development and verification. While feature-based strategies to verify
    features in isolation have existed for years, they cannot address interactions
    between features. The problem with feature interactions is that they are typically
    unknown and may involve any subset of the features. Contrary, a family-based verification
    strategy captures feature interactions, but does not scale well when features
    evolve frequently. To the best of our knowledge, there currently exists no approach
    with focus on evolving features that combines both strategies and aims at eliminating
    their respective drawbacks. To fill this gap, we introduce Fefalution, a feature-family-based
    verification approach based on abstract contracts to verify evolving features
    and their interactions. Fefalution builds partial proofs for each evolving feature
    and then reuses the resulting partial proofs in verifying feature interactions,
    yielding a full verification of the complete software system. Moreover, to investigate
    whether a combination of both strategies is fruitful, we present the first empirical
    study for the verification of evolving features implemented by means of feature-oriented
    programming and by comparing Fefalution with another five family-based approaches
    varying in a set of optimizations. Our results indicate that partial proofs based
    on abstract contracts exhibit huge reuse potential, but also come with a substantial
    overhead for smaller evolution scenarios.\r\n"
author:
- first_name: Alexander
  full_name: Knüppel, Alexander
  last_name: Knüppel
- first_name: Stefan
  full_name: Krüger, Stefan
  last_name: Krüger
- first_name: Thomas
  full_name: Thüm, Thomas
  last_name: Thüm
- first_name: Richard
  full_name: Bubel, Richard
  last_name: Bubel
- first_name: Sebastian
  full_name: Krieter, Sebastian
  last_name: Krieter
- first_name: Eric
  full_name: Bodden, Eric
  id: '59256'
  last_name: Bodden
  orcid: 0000-0003-3470-3647
- first_name: Ina
  full_name: Schaefer, Ina
  last_name: Schaefer
citation:
  ama: 'Knüppel A, Krüger S, Thüm T, et al. Using Abstract Contracts for Verifying
    Evolving Features and Their Interactions. In: <i>Lecture Notes in Computer Science</i>.
    ; 2020. doi:<a href="https://doi.org/10.1007/978-3-030-64354-6_5">10.1007/978-3-030-64354-6_5</a>'
  apa: Knüppel, A., Krüger, S., Thüm, T., Bubel, R., Krieter, S., Bodden, E., &#38;
    Schaefer, I. (2020). Using Abstract Contracts for Verifying Evolving Features
    and Their Interactions. In <i>Lecture Notes in Computer Science</i>. <a href="https://doi.org/10.1007/978-3-030-64354-6_5">https://doi.org/10.1007/978-3-030-64354-6_5</a>
  bibtex: '@inbook{Knüppel_Krüger_Thüm_Bubel_Krieter_Bodden_Schaefer_2020, place={Cham},
    title={Using Abstract Contracts for Verifying Evolving Features and Their Interactions},
    DOI={<a href="https://doi.org/10.1007/978-3-030-64354-6_5">10.1007/978-3-030-64354-6_5</a>},
    booktitle={Lecture Notes in Computer Science}, author={Knüppel, Alexander and
    Krüger, Stefan and Thüm, Thomas and Bubel, Richard and Krieter, Sebastian and
    Bodden, Eric and Schaefer, Ina}, year={2020} }'
  chicago: Knüppel, Alexander, Stefan Krüger, Thomas Thüm, Richard Bubel, Sebastian
    Krieter, Eric Bodden, and Ina Schaefer. “Using Abstract Contracts for Verifying
    Evolving Features and Their Interactions.” In <i>Lecture Notes in Computer Science</i>.
    Cham, 2020. <a href="https://doi.org/10.1007/978-3-030-64354-6_5">https://doi.org/10.1007/978-3-030-64354-6_5</a>.
  ieee: A. Knüppel <i>et al.</i>, “Using Abstract Contracts for Verifying Evolving
    Features and Their Interactions,” in <i>Lecture Notes in Computer Science</i>,
    Cham, 2020.
  mla: Knüppel, Alexander, et al. “Using Abstract Contracts for Verifying Evolving
    Features and Their Interactions.” <i>Lecture Notes in Computer Science</i>, 2020,
    doi:<a href="https://doi.org/10.1007/978-3-030-64354-6_5">10.1007/978-3-030-64354-6_5</a>.
  short: 'A. Knüppel, S. Krüger, T. Thüm, R. Bubel, S. Krieter, E. Bodden, I. Schaefer,
    in: Lecture Notes in Computer Science, Cham, 2020.'
date_created: 2021-01-11T09:15:41Z
date_updated: 2022-01-06T06:54:41Z
department:
- _id: '76'
doi: 10.1007/978-3-030-64354-6_5
language:
- iso: eng
place: Cham
publication: Lecture Notes in Computer Science
publication_identifier:
  isbn:
  - '9783030643539'
  - '9783030643546'
  issn:
  - 0302-9743
  - 1611-3349
publication_status: published
status: public
title: Using Abstract Contracts for Verifying Evolving Features and Their Interactions
type: book_chapter
user_id: '5786'
year: '2020'
...