Family-Based Deductive Verification of Software Product Lines

被引：23

作者：

Thuem, Thomas ^{[1
]}

Schaefer, Ina ^{[2
]}

Apel, Sven ^{[3
]}

Hentschel, Martin ^{[4
]}

机构：

[1] Univ Magdeburg, D-39106 Magdeburg, Germany

[2] Tech Univ Carolo Wilhelmina Braunschweig, Braunschweig, Germany

[3] Univ Passau, Passau, Germany

[4] Tech Univ Darmstadt, Darmstadt, Germany

来源：

ACM SIGPLAN NOTICES | 2013年 / 48卷 / 03期

关键词：

Reliability; Verification; Product-line analysis; software product lines; program families; deductive verification; theorem proving; MODEL CHECKING;

D O I：

10.1145/2480361.2371404

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e. g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used off-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %.

引用

页码：11 / 20

页数：10

共 50 条

[41] CAOVerif: An open-source deductive verification platform for cryptographic software implementations
Almeida, Jose Bacelar
Barbosa, Manuel
Filliatre, Jean-Christophe
Pinto, Jorge Sousa
Vieira, Barbara
SCIENCE OF COMPUTER PROGRAMMING, 2014, 91 : 216 - 233
[42] Key activities for product derivation in software product lines
Rabiser, Rick
O'Leary, Padraig
Richardson, Ita
JOURNAL OF SYSTEMS AND SOFTWARE, 2011, 84 (02) : 285 - 300
[43] Automatic and Incremental Product Optimization for Software Product Lines
Demuth, Andreas
Lopez-Herrejon, Roberto E.
Egyed, Alexander
2014 IEEE SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), 2014, : 31 - 40
[44] Tailoring Dynamic Software Product Lines
Rosenmueller, Marko
Siegmund, Norbert
Pukall, Mario
Apel, Sven
GPCE 11: PROCEEDINGS OF THE TENTH INTERNATIONAL CONFERENCE ON GENERATIVE PROGRAMMING AND COMPONENT ENGINEERING, 2011, : 3 - 12
[45] A formal framework for software product lines
Andres, Cesar
Camacho, Carlos
Llana, Luis
INFORMATION AND SOFTWARE TECHNOLOGY, 2013, 55 (11) : 1925 - 1947
[46] Integrated software process and product lines
Rombach, D
UNIFYING THE SOFTWARE PROCESS SPECTRUM, 2005, 3840 : 83 - 90
[47] Unburdening onboarding in Software Product Lines
Medeiros, Raul
2021 IEEE/ACM 43RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS (ICSE-COMPANION 2021), 2021, : 260 - 262
[48] Toward Compositional Software Product Lines
Bosch, Jan
IEEE SOFTWARE, 2010, 27 (03) : 29 - 34
[49] Tailoring Dynamic Software Product Lines
Rosenmueller, Marko
Siegmund, Norbert
Pukall, Mario
Apel, Sven
ACM SIGPLAN NOTICES, 2012, 47 (03) : 3 - 12
[50] Classification-based Mining of Reusable Components on Software Product Lines
Arias, M.
De Renzis, A.
Buccella, A.
Flores, A.
Cechich, A.
IEEE LATIN AMERICA TRANSACTIONS, 2016, 14 (02) : 870 - 876

← 1 2 3 4 5 →