CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verification of Software Product Lines with Delta-oriented Slicing

Daniel Bruns ; Vladimir Klebanov ; Ina Schaefer (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science. International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2010, Paris, 28-30 June 2010 (0302-9743). Vol. 6528 (2011), p. 61-75.
[Konferensbidrag, refereegranskat]

Software product line (SPL) engineering is a well-known approach to develop industry-size adaptable software systems. SPL are often used in domains where high-quality software is desirable; the overwhelming product diversity, however, remains a challenge for assuring correctness. In this paper, we present delta-oriented slicing, an approach to reduce the deductive verification effort across an SPL where individual products are Java programs and their relations are described by deltas. On the specification side, we extend the delta language to deal with formal specifications. On the verification side, we combine proof slicing and similarity-guided proof reuse to ease the verification process.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2010-12-20. Senast ändrad 2012-02-15.
CPL Pubid: 131316