Compositional Verification of Evolving SPL - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2012

Compositional Verification of Evolving SPL

Résumé

This paper presents a novel approach to the design verification of Software Product Lines(SPL). The proposed approach assumes that the requirements and designs are modeled as finite state machines with variability information. The variability information at the requirement and design levels are expressed differently and at different levels of abstraction. Also the proposed approach supports verification of SPL in which new features and variability may be added incrementally. Given the design and requirements of an SPL, the proposed design verification method ensures that every product at the design level behaviorally conforms to a product at the requirement level. The conformance procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. The method has been implemented and demonstrated in a prototype tool SPLEnD (SPL Engine for Design Verification) on a couple of fairly large case studies.
Ce papier présente une approche nouvelle de vérification pour les lignes de produits logiciels (LPL). L'approche proposée considère que la spécification et la conception de LPL peuvent être abstraites comme des automates à états finis comprenant des informations sur la variabilité. Ces informations sont exprimées différemment aux niveaux spécification et conceptions. Sous ces hypothèses, l'approche proposée supporte la vérification de LPLs dans lesquelles des fonctionnalités peuvent être ajoutées incrémentalement. A partir de la spécification et de la conception d'une LPL, la méthode de vérification proposée assure que chaque produit au niveau conception se conforme, comportementalement parlant, à un produit au niveau spécification. La procédure de conformité est compositionnelle car la vérification de la LPL en entier se réduit à la vérification des fonctionnalités qui la compose individuellement. La méthode a été implantée dans un outil appelé ''SPLEnD'' et essayée sur deux cas d'étude relativement larges.
Fichier principal
Vignette du fichier
mainRR8125.pdf (2 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00747533 , version 1 (31-10-2012)

Identifiants

  • HAL Id : hal-00747533 , version 1

Citer

Jean-Vivien Millo, S. Ramesh, Shankara Narayanan Krishna, Ganesh Khandu Narwane. Compositional Verification of Evolving SPL. [Research Report] RR-8125, INRIA. 2012, pp.34. ⟨hal-00747533⟩
228 Consultations
406 Téléchargements

Partager

Gmail Facebook X LinkedIn More