kth.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Compositional Algorithmic Verification of Software Product Lines
Technische Universität Braunschweig, Germany.
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0002-0074-8786
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
2010 (Engelska)Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Springer, 2010. s. 184-203
Serie
Lecture notes in computer science, ISSN 0302-9743 ; 6957
Nyckelord [en]
Distributed systems, event-B, fault injection, model checking, software verification
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:kth:diva-49419DOI: 10.1007/978-3-642-25271-6_10Scopus ID: 2-s2.0-84255161819ISBN: 978-3-642-25270-9 (tryckt)OAI: oai:DiVA.org:kth-49419DiVA, id: diva2:459635
Konferens
9th International Symposium on Formal Methods for Components and Objects, FMCO 2010; Graz; Austria; 29 November-1 December 2010
Anmärkning

QC 20140915

Tillgänglig från: 2012-01-09 Skapad: 2011-11-27 Senast uppdaterad: 2024-03-18Bibliografiskt granskad

Open Access i DiVA

fmco(449 kB)371 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 449 kBChecksumma SHA-512
302d4be9d04a9744a5c17e292db31b4fa8391243b0376c2f0d27f248d712c1707eeb636ea48e67561748a4df47c2ec93550e859be89c0664b3e93a87a80d1642
Typ fulltextMimetyp application/pdf

Övriga länkar

Förlagets fulltextScopusThe final publication is available at www.springerlink.com

Person

Gurov, DilianSoleimanifard, Siavash

Sök vidare i DiVA

Av författaren/redaktören
Gurov, DilianSoleimanifard, Siavash
Av organisationen
Teoretisk datalogi, TCS
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 371 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 172 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf