Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specications in a delta module describe changes to previous specications. Our approach allows each delta module to be veried in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specications of this product variant.

A Transformational Proof System for Delta-Oriented Programming

DAMIANI, Ferruccio;
2012-01-01

Abstract

Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specications in a delta module describe changes to previous specications. Our approach allows each delta module to be veried in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specications of this product variant.
2012
Third International Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE)
Salvador, Brazil
September 2, 2012
Proceedings of the 16th International Software Product Line Conference - Volume 2
ACM
2
53
60
9781450310956
http://dl.acm.org/citation.cfm?doid=2364412.2364422
http://dl.acm.org/citation.cfm?id=2364412&picked=prox&CFID=156527608&CFTOKEN=44588838
http://www.iese.fraunhofer.de/en/events/fmsple2012.html
Program Verication; Proof System; Software Product Line
Ferruccio Damiani; Johan Dovland; Einar Broch Johnsen; Olaf Owe; Ina Schaefer; Ingrid Chieh Yu
File in questo prodotto:
File Dimensione Formato  
paper-145.pdf

Accesso riservato

Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 438.95 kB
Formato Adobe PDF
438.95 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/115975
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 26
  • ???jsp.display-item.citation.isi??? ND
social impact