TU Darmstadt / ULB / TUbiblio

Delta-based verification of software product families

Scaletta, Marco ; Hähnle, Reiner ; Steinhöfel, Dominic ; Bubel, Richard
Tilevich, Eli ; Roover, Coen De (eds.) (2021):
Delta-based verification of software product families.
In: GPCE 2021: Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, pp. 69-82,
ACM, 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, Chicago, USA, 17.-18.10.2021, ISBN 978-1-4503-9112-2,
DOI: 10.1145/3486609.3487200,
[Conference or Workshop Item]

Abstract

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.

Item Type: Conference or Workshop Item
Erschienen: 2021
Editors: Tilevich, Eli ; Roover, Coen De
Creators: Scaletta, Marco ; Hähnle, Reiner ; Steinhöfel, Dominic ; Bubel, Richard
Title: Delta-based verification of software product families
Language: English
Abstract:

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.

Book Title: GPCE 2021: Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences
Publisher: ACM
ISBN: 978-1-4503-9112-2
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Event Title: 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences
Event Location: Chicago, USA
Event Dates: 17.-18.10.2021
Date Deposited: 20 Jul 2022 07:02
DOI: 10.1145/3486609.3487200
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)
Show editorial Details Show editorial Details