Towards an incremental automata-based approach for software product-line model checking

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceChapitre

84 Téléchargements (Pure)

Résumé

Most model-checking algorithms are based on automata theory. For instance, determining whether or not a transition system satisfies a Linear Temporal Logic (LTL) formula requires computing strongly connected component of its transition graph. In Software Product-Line (SPL) engineering, the model checking problem is more complex due to the huge amount of software products that may compose the line. Indeed, one has to determine the exact subset of those products that do not satisfy an intended property. Efficient dedicated verification methods have been recently developed to answer this problem. However, most of them does not allow incremental verification. In this paper, we introduce an automata-based incremental approach for SPL model checking. Our method makes use of previous results to determine whether or not the addition of conservative features (i.e., features that do not remove behaviour from the system) preserves the satisfaction of properties expressed in LTL. We provide a detailed description of the approach and propose algorithms that implement it. We discuss how our method can be combined with SPL dedicated verification methods, viz. Featured Transition Systems. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification- Model checking General Terms Theory, Verification.
langue originaleAnglais
titreACM International Conference Proceeding Series
Pages74-81
Nombre de pages8
Volume2
Les DOIs
Etat de la publicationPublié - 1 janv. 2012

Empreinte digitale

Examiner les sujets de recherche de « Towards an incremental automata-based approach for software product-line model checking ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation