ProVeLines: A Product Line of Verifiers for Software Product Lines

Maxime Cordy; Andreas Classen; Patrick Heymans; Pierre-Yves Schobbens; Axel Legay

doi:10.1145/2499777.2499781

ProVeLines: A Product Line of Verifiers for Software Product Lines

Maxime Cordy, Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay

Research output: Contribution to conference › Paper › peer-review

Abstract

Software Product Lines (SPLs) are families of similar software products built from a common set of features. As the number of products of an SPL is potentially exponential in the number of its features, the model checking problem is harder than for single software. A practical way to face this exponential blow-up is to reuse common behaviour between products. We previously introduced Featured Transition Systems (FTS), a mathematical model that serves as a basis for efficient SPL model checking techniques. In this paper, we present ProVeLines, a product line of verifiers for SPLs that incorporates the results of over three years of research on formal verification of SPLs. Being itself a product line, our tool is flexible and extensible, and offers a wide range of solutions for SPL modelling and verification. Copyright 2013 ACM.

Original language	English
Pages	141 - 146
Number of pages	6
DOIs	https://doi.org/10.1145/2499777.2499781
Publication status	Published - Aug 2013
Event	17th International Software Product Line Conference - Tokyo, Tokyo, Japan Duration: 26 Aug 2013 → 30 Aug 2013

Conference

Conference	17th International Software Product Line Conference
Country/Territory	Japan
City	Tokyo
Period	26/08/13 → 30/08/13

Keywords

Software Product Line Engineering

Access to Document

10.1145/2499777.2499781

http://www.scopus.com/inward/record.url?eid=2-s2.0-84890468592&partnerID=8YFLogxK

Thesis-M-Cordy: Modular Modelling and Verification of Real-Time Software Product Lines
CORDY, M., Heymans, P. & Schobbens, P. Y.
1/10/11 → 30/09/15
Project: PHD
TPA: Theory and Practice of Automata and Logics
Schobbens, P. Y., CORDY, M., KANG, E. & Ortiz Vega, J. J.
1/01/11 → 31/12/14
Project: Research
VLPL: Software Product Lines Verification
Heymans, P., Schobbens, P. Y., Classen, A., CORDY, M., KANG, E. & Legay, A.
1/01/11 → 1/01/13
Project: Research

Cite this

@conference{1021a56170004af0a679f7cdbb348490,

title = "ProVeLines: A Product Line of Verifiers for Software Product Lines",

abstract = "Software Product Lines (SPLs) are families of similar software products built from a common set of features. As the number of products of an SPL is potentially exponential in the number of its features, the model checking problem is harder than for single software. A practical way to face this exponential blow-up is to reuse common behaviour between products. We previously introduced Featured Transition Systems (FTS), a mathematical model that serves as a basis for efficient SPL model checking techniques. In this paper, we present ProVeLines, a product line of verifiers for SPLs that incorporates the results of over three years of research on formal verification of SPLs. Being itself a product line, our tool is flexible and extensible, and offers a wide range of solutions for SPL modelling and verification. Copyright 2013 ACM.",

keywords = "Software Product Line Engineering",

author = "Maxime Cordy and Andreas Classen and Patrick Heymans and Pierre-Yves Schobbens and Axel Legay",

year = "2013",

month = aug,

doi = "10.1145/2499777.2499781",

language = "English",

pages = "141 -- 146",

note = "17th International Software Product Line Conference ; Conference date: 26-08-2013 Through 30-08-2013",

}

TY - CONF

T1 - ProVeLines

T2 - 17th International Software Product Line Conference

AU - Cordy, Maxime

AU - Classen, Andreas

AU - Heymans, Patrick

AU - Schobbens, Pierre-Yves

AU - Legay, Axel

PY - 2013/8

Y1 - 2013/8

N2 - Software Product Lines (SPLs) are families of similar software products built from a common set of features. As the number of products of an SPL is potentially exponential in the number of its features, the model checking problem is harder than for single software. A practical way to face this exponential blow-up is to reuse common behaviour between products. We previously introduced Featured Transition Systems (FTS), a mathematical model that serves as a basis for efficient SPL model checking techniques. In this paper, we present ProVeLines, a product line of verifiers for SPLs that incorporates the results of over three years of research on formal verification of SPLs. Being itself a product line, our tool is flexible and extensible, and offers a wide range of solutions for SPL modelling and verification. Copyright 2013 ACM.

AB - Software Product Lines (SPLs) are families of similar software products built from a common set of features. As the number of products of an SPL is potentially exponential in the number of its features, the model checking problem is harder than for single software. A practical way to face this exponential blow-up is to reuse common behaviour between products. We previously introduced Featured Transition Systems (FTS), a mathematical model that serves as a basis for efficient SPL model checking techniques. In this paper, we present ProVeLines, a product line of verifiers for SPLs that incorporates the results of over three years of research on formal verification of SPLs. Being itself a product line, our tool is flexible and extensible, and offers a wide range of solutions for SPL modelling and verification. Copyright 2013 ACM.

KW - Software Product Line Engineering

U2 - 10.1145/2499777.2499781

DO - 10.1145/2499777.2499781

M3 - Paper

SP - 141

EP - 146

Y2 - 26 August 2013 through 30 August 2013

ER -

ProVeLines: A Product Line of Verifiers for Software Product Lines

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

Thesis-M-Cordy: Modular Modelling and Verification of Real-Time Software Product Lines

TPA: Theory and Practice of Automata and Logics

VLPL: Software Product Lines Verification

Cite this