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 条

[31] Family-Based Benchmarking of Copy Number Variation Detection Software
Nutsua, Marcel Elie
Fischer, Annegret
Nebel, Almut
Hofmann, Sylvia
Schreiber, Stefan
Krawczak, Michael
Nothnagel, Michael
PLOS ONE, 2015, 10 (07):
[32] Software product lines
Bosch, J
TECHNOLOGY OF OBJECT-ORIENTED LANGUAGES - TOOLS 33, PROCEEDINGS, 2000, : 467 - 467
[33] A study: selection of model metamodel and SPL tools for the verification of software product lines
Khan F.Q.
Musa S.
Tsaramirsis G.
Bakhsh S.T.
International Journal of Information Technology, 2017, 9 (4) : 353 - 362
[34] Survey of Non-Functional Requirements Modeling and Verification of Software Product Lines
Hammani, Fatima Zahra
2014 IEEE EIGHTH INTERNATIONAL CONFERENCE ON RESEARCH CHALLENGES IN INFORMATION SCIENCE (RCIS), 2014,
[35] Integrating object-oriented design and deductive verification of software
Beckert, Bernhard
Haehnle, Reiner
Schmitt, Peter H.
SEFM 2006: FOURTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2006, : 260 - 260
[36] Verification of Migrated Product Lines
Mukelabai, Mukelabai
SPLC'18: PROCEEDINGS OF THE 22ND INTERNATIONAL SYSTEMS AND SOFTWARE PRODUCT LINE CONFERENCE - VOL 2, 2018, : 87 - 89
[37] Product Feasibility Verification in Software Product Line
Cristian Martinez, Omar
Gonnet, Silvio
Leone, Horacio
Diaz, Nicolas
2012 XXXVIII CONFERENCIA LATINOAMERICANA EN INFORMATICA (CLEI), 2012,
[38] FIG based Quality Assurance in Software Product Lines
Yousaf, Nazish
Sheikh, Rida
Abbas, Muhammad
2017 INTERNATIONAL CONFERENCE ON FRONTIERS OF INFORMATION TECHNOLOGY (FIT), 2017, : 173 - 177
[39] 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
[40] Specification-based Testing for Software Product Lines
Kahsai, Temesghen
Roggenbach, Markus
Schlingloff, Bernd-Holger
SEFM 2008: SIXTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2008, : 149 - +

← 1 2 3 4 5 →