Delta-based Verification of Software Product FamiliesVirtual
Mon 18 Oct 2021 16:25 - 16:40 at Zurich C - SLE/GPCE Session 8 Chair(s): Ran Wei
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.
Mon 18 OctDisplayed time zone: Central Time (US & Canada) change
07:40 - 09:00 | |||
07:40 15mTalk | Leveraging Relational Concept Analysis for Automated Feature Location in Software Product LinesVirtual GPCE Nicolas Hlad LIRMM, CNRS, Bérénice Lemoine LIRMM, CNRS, Marianne Huchard LIRMM, Abdelhak Seriai LIRMM, CNRS and University of Montpellier | ||
07:55 15mTalk | FIDDLR: Streamlining Reuse with Concern-Specific Modelling LanguagesVirtual SLE Maximilian Schiedermeier McGill University, Jörg Kienzle McGill University, Canada, Bettina Kemme McGill University, Canada | ||
08:10 15mTalk | Lifted Termination Analysis by Abstract Interpretation and its ApplicationsVirtual GPCE Aleksandar S. Dimovski Mother Teresa University, Skopje | ||
08:25 15mTalk | Delta-based Verification of Software Product FamiliesVirtual GPCE Marco Scaletta Technische Universität Darmstadt, Reiner Hähnle Technical University of Darmstadt, Dominic Steinhöfel CISPA Helmholtz Center for Information Security, Richard Bubel Technische Universität Darmstadt | ||
08:40 20mLive Q&A | Discussion, Questions and Answers SLE |
15:40 - 17:00 | |||
15:40 15mTalk | Leveraging Relational Concept Analysis for Automated Feature Location in Software Product LinesVirtual GPCE Nicolas Hlad LIRMM, CNRS, Bérénice Lemoine LIRMM, CNRS, Marianne Huchard LIRMM, Abdelhak Seriai LIRMM, CNRS and University of Montpellier | ||
15:55 15mTalk | FIDDLR: Streamlining Reuse with Concern-Specific Modelling LanguagesVirtual SLE Maximilian Schiedermeier McGill University, Jörg Kienzle McGill University, Canada, Bettina Kemme McGill University, Canada | ||
16:10 15mTalk | Lifted Termination Analysis by Abstract Interpretation and its ApplicationsVirtual GPCE Aleksandar S. Dimovski Mother Teresa University, Skopje | ||
16:25 15mTalk | Delta-based Verification of Software Product FamiliesVirtual GPCE Marco Scaletta Technische Universität Darmstadt, Reiner Hähnle Technical University of Darmstadt, Dominic Steinhöfel CISPA Helmholtz Center for Information Security, Richard Bubel Technische Universität Darmstadt | ||
16:40 20mLive Q&A | Discussion, Questions and Answers SLE |