Formal semantics, modular specification, and symbolic verification of product-line behaviour

Research output: Contribution to journalArticle

159 Downloads (Pure)

Abstract

Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated algorithms, SPL model checking still faces the well-known state explosion problem. Moreover, there is a need for high-level specification languages usable in industry. We address the state explosion problem by applying the principles of symbolic model checking to FTS-based verification of SPLs. In order to specify properties on specific products only, we extend the temporal logic CTL with feature quantifiers. Next, we show how SPL behaviour can be specified with fSMV, a variant of SMV, the specification language of the industry-strength model checker NuSMV. fSMV is a feature-oriented extension of SMV originally introduced by Plath and Ryan. We prove that fSMV and FTSs are expressively equivalent. Finally, we connect these results to a NuSMV extension we developed for verifying SPLs against CTL properties.

Original languageEnglish
Pages (from-to)416-439
Number of pages24
JournalScience of Computer Programming
Volume80
Issue numberPART B
DOIs
Publication statusPublished - 1 Feb 2014

Fingerprint

Specification languages
Model checking
Explosions
Semantics
Specifications
Temporal logic
Industry

Keywords

  • Feature
  • Language
  • Software product line
  • Specification
  • Verification

Cite this

@article{3be87429e33e41dfbbe819416b9b494b,
title = "Formal semantics, modular specification, and symbolic verification of product-line behaviour",
abstract = "Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated algorithms, SPL model checking still faces the well-known state explosion problem. Moreover, there is a need for high-level specification languages usable in industry. We address the state explosion problem by applying the principles of symbolic model checking to FTS-based verification of SPLs. In order to specify properties on specific products only, we extend the temporal logic CTL with feature quantifiers. Next, we show how SPL behaviour can be specified with fSMV, a variant of SMV, the specification language of the industry-strength model checker NuSMV. fSMV is a feature-oriented extension of SMV originally introduced by Plath and Ryan. We prove that fSMV and FTSs are expressively equivalent. Finally, we connect these results to a NuSMV extension we developed for verifying SPLs against CTL properties.",
keywords = "Feature, Language, Software product line, Specification, Verification",
author = "Andreas Classen and Maxime Cordy and Patrick Heymans and Axel Legay and Schobbens, {Pierre Yves}",
year = "2014",
month = "2",
day = "1",
doi = "10.1016/j.scico.2013.09.019",
language = "English",
volume = "80",
pages = "416--439",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",
number = "PART B",

}

TY - JOUR

T1 - Formal semantics, modular specification, and symbolic verification of product-line behaviour

AU - Classen, Andreas

AU - Cordy, Maxime

AU - Heymans, Patrick

AU - Legay, Axel

AU - Schobbens, Pierre Yves

PY - 2014/2/1

Y1 - 2014/2/1

N2 - Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated algorithms, SPL model checking still faces the well-known state explosion problem. Moreover, there is a need for high-level specification languages usable in industry. We address the state explosion problem by applying the principles of symbolic model checking to FTS-based verification of SPLs. In order to specify properties on specific products only, we extend the temporal logic CTL with feature quantifiers. Next, we show how SPL behaviour can be specified with fSMV, a variant of SMV, the specification language of the industry-strength model checker NuSMV. fSMV is a feature-oriented extension of SMV originally introduced by Plath and Ryan. We prove that fSMV and FTSs are expressively equivalent. Finally, we connect these results to a NuSMV extension we developed for verifying SPLs against CTL properties.

AB - Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated algorithms, SPL model checking still faces the well-known state explosion problem. Moreover, there is a need for high-level specification languages usable in industry. We address the state explosion problem by applying the principles of symbolic model checking to FTS-based verification of SPLs. In order to specify properties on specific products only, we extend the temporal logic CTL with feature quantifiers. Next, we show how SPL behaviour can be specified with fSMV, a variant of SMV, the specification language of the industry-strength model checker NuSMV. fSMV is a feature-oriented extension of SMV originally introduced by Plath and Ryan. We prove that fSMV and FTSs are expressively equivalent. Finally, we connect these results to a NuSMV extension we developed for verifying SPLs against CTL properties.

KW - Feature

KW - Language

KW - Software product line

KW - Specification

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=84889886727&partnerID=8YFLogxK

U2 - 10.1016/j.scico.2013.09.019

DO - 10.1016/j.scico.2013.09.019

M3 - Article

VL - 80

SP - 416

EP - 439

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

IS - PART B

ER -