Compositional Verification of Evolving SPL

Résumé : 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.
Type de document :
Rapport
[Research Report] RR-8125, INRIA. 2012, pp.34


https://hal.inria.fr/hal-00747533
Contributeur : Team Aoste <>
Soumis le : mercredi 31 octobre 2012 - 14:58:44
Dernière modification le : samedi 17 septembre 2016 - 01:36:48

Fichiers

mainRR8125.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00747533, version 1

Collections

Citation

Jean-Vivien Millo, S. Ramesh, Shankara Krishna, Ganesh Narwane. Compositional Verification of Evolving SPL. [Research Report] RR-8125, INRIA. 2012, pp.34. <hal-00747533>

Exporter

Partager

Métriques

Consultations de
la notice

220

Téléchargements du document

216