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 条

[21] Search Based Design of Software Product Lines Architectures
Colanzi, Thelma Elita
2012 34TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2012, : 1507 - 1510
[22] TESTING IN SOFTWARE PRODUCT LINES A Model based Approach
Reales Mateo, Pedro
Polo Usaola, Macario
Caivano, Danilo
ICEIS 2011: PROCEEDINGS OF THE 13TH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS, VOL 3, 2011, : 46 - 54
[23] Intraprocedural Dataflow Analysis for Software Product Lines
Brabrand, Claus
Ribeiro, Marcio
Toledo, Tarsis
Winther, Johnni
Borba, Paulo
TRANSACTIONS ON ASPECT-ORIENTED SOFTWARE DEVELOPMENT X, 2013, 7800 : 73 - 108
[24] Two-Step Deductive Verification of Control Software Using Reflex
Anureev, Igor
Garanina, Natalia
Liakh, Tatiana
Rozov, Andrei
Zyubin, Vladimir
Gorlatch, Sergei
PERSPECTIVES OF SYSTEM INFORMATICS (PSI 2019), 2019, 11964 : 50 - 63
[25] Probabilistic software product lines
Camacho, Carlos
Llana, Luis
Nunez, Alberto
Bravetti, Mario
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2019, 107 : 54 - 78
[26] Sustainability in Software Product Lines
Chitchyan, Ruzanna
Noppen, Joost
Groher, Iris
18TH INTERNATIONAL SOFTWARE PRODUCT LINE CONFERENCE (SPLC 2014), VOL 1, 2014, : 367 - 367
[27] Learning by sampling: learning behavioral family models from software product lines
Nascimento Damasceno, Carlos Diego
Mousavi, Mohammad Reza
Simao, Adenilso da Silva
EMPIRICAL SOFTWARE ENGINEERING, 2021, 26 (01)
[28] Learning by sampling: learning behavioral family models from software product lines
Carlos Diego Nascimento Damasceno
Mohammad Reza Mousavi
Adenilso da Silva Simao
Empirical Software Engineering, 2021, 26
[29] Granularity in Software Product Lines
Kaestner, Christian
Apel, Sven
Kuhlemann, Martin
ICSE'08 PROCEEDINGS OF THE THIRTIETH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2008, : 311 - 320
[30] Testing Software Product Lines
da Mota Silveira Neto, Paulo Anselmo
Runeson, Per
Machado, Ivan do Carmo
de Almeida, Eduardo Santana
de Lemos Meira, Silvio Romero
Engstrom, Emelie
IEEE SOFTWARE, 2011, 28 (05) : 16 - 20

← 1 2 3 4 5 →