Change search
ReferencesLink to record
Permanent link

Direct link
Compositional Algorithmic Verification of Software Product Lines
Technische Universität Braunschweig, Germany.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2010 (English)Conference paper (Refereed)
Abstract [en]

Software product line engineering allows large software systems to be developed and adapted for varying customer needs. The products of a software product line can be described by means of a {\em hierarchical variability model} specifying the commonalities and variabilities between the artifacts of the individual products. The number of products generated by a hierarchical model is exponential in its size, which poses a serious challenge to software product line analysis and verification. For an analysis technique to scale, the effort has to be linear in the size of the model rather than linear in the number of products it generates. Hence, efficient product line verification is only possible if {\em compositional} verification techniques are applied that allow the analysis of products to be {\em relativized}  on the properties of their variation points. In this paper, we propose simple hierarchical variability models (SHVM) with explicit variation points as a novel way to describe a set of products consisting of sets of methods. SHVMs provide a trade--off between expressiveness and a clean and simple model suitable for compositional verification. We generalize a previously developed  compositional technique and tool set for the automatic verification of control--flow based temporal safety properties to product lines defined by SHVMs, and prove soundness of the generalization. The desired property relativization is achieved by introducing variation point specifications. We evaluate the proposed technique on a number of test cases.

Place, publisher, year, edition, pages
Springer, 2010. 184-203 p.
, Lecture notes in computer science, ISSN 03029743 ; 6957
Keyword [en]
Distributed systems, event-B, fault injection, model checking, software verification
National Category
Computer Science
URN: urn:nbn:se:kth:diva-49419DOI: 10.1007/978-3-642-25271-6_10ScopusID: 2-s2.0-84255161819ISBN: 978-3-642-25270-9OAI: diva2:459635
9th International Symposium on Formal Methods for Components and Objects, FMCO 2010; Graz; Austria; 29 November-1 December 2010

QC 20140915

Available from: 2012-01-09 Created: 2011-11-27 Last updated: 2014-09-15Bibliographically approved

Open Access in DiVA

fmco(449 kB)115 downloads
File information
File name FULLTEXT01.pdfFile size 449 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopusThe final publication is available at

Search in DiVA

By author/editor
Gurov, DilianSoleimanifard, Siavash
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 115 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 50 hits
ReferencesLink to record
Permanent link

Direct link