CISPA
Browse
- No file added yet -

Delta-based Verification of Software Product Families

Download (648.63 kB)
conference contribution
posted on 2023-11-29, 18:17 authored by Marco Scaletta, Reiner Hähnle, Dominic Steinhöfel, Richard Bubel
The quest for feature- and family-oriented deductive verification of software product lines resulted in several proposals. In this paper we look at delta-oriented modeling of product lines and combine two new ideas: first, we extend Hähnle & Schaefer’s delta-oriented version of Liskov’s substitution principle for behavioral subtyping to work also for overridden behavior in benign cases. For this to succeed, programs need to be in a certain normal form. The required normal form turns out to be achievable in many cases by a set of program transformations, whose correctness is ensured by the recent technique of abstract execution. This is a generalization of symbolic execution that permits reasoning about abstract code elements. It is needed, because code deltas contain partially unknown code contexts in terms of “original” calls. Second, we devise a modular verification procedure for deltas based on abstract execution, representing deltas as abstract programs calling into unknown contexts. The result is a “delta-based” verification approach, where each modification of a method in a code delta is verified in isolation, but which overcomes the strict limitations of behavioral subtyping and works for many practical programs. The latter claim is substantiated with case studies and benchmarks.

History

Preferred Citation

Marco Scaletta, Reiner Hähnle, Dominic Steinhöfel and Richard Bubel. Delta-based Verification of Software Product Families. In: International Conference on Generative Programming: Concepts & Experiences (GPCE). 2021.

Primary Research Area

  • Empirical and Behavioral Security

Name of Conference

International Conference on Generative Programming: Concepts & Experiences (GPCE)

Legacy Posted Date

2021-10-19

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3509, title = "Delta-based Verification of Software Product Families", author = "Scaletta, Marco and Hähnle, Reiner and Steinhöfel, Dominic and Bubel, Richard", booktitle="{International Conference on Generative Programming: Concepts & Experiences (GPCE)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC