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

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

Résultats de recherche: Contribution à un journal/une revueArticleRevue par des pairs

421 Téléchargements (Pure)

Résumé

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.

langue originaleAnglais
Pages (de - à)416-439
Nombre de pages24
journalScience of Computer Programming
Volume80
Numéro de publicationPART B
Les DOIs
Etat de la publicationPublié - 1 févr. 2014

Empreinte digitale

Examiner les sujets de recherche de « Formal semantics, modular specification, and symbolic verification of product-line behaviour ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation