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

Research output: Contribution in Book/Catalog/Report/Conference proceedingChapter

69 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationACM International Conference Proceeding Series
Pages74-81
Number of pages8
Volume2
DOIs
Publication statusPublished - 1 Jan 2012

Fingerprint

Model checking
Temporal logic
Automata theory
Software engineering

Cite this

@inbook{fcf37ba552594c9ea48306775d8b3f4a,
title = "Towards an incremental automata-based approach for software product-line model checking",
abstract = "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.",
author = "Maxime Cordy and Pierre Schobbens and Patrick Heymans and Axel Legay",
year = "2012",
month = "1",
day = "1",
doi = "10.1145/2364412.2364425",
language = "English",
isbn = "9781450310956",
volume = "2",
pages = "74--81",
booktitle = "ACM International Conference Proceeding Series",

}

Towards an incremental automata-based approach for software product-line model checking. / Cordy, Maxime; Schobbens, Pierre; Heymans, Patrick; Legay, Axel.

ACM International Conference Proceeding Series. Vol. 2 2012. p. 74-81.

Research output: Contribution in Book/Catalog/Report/Conference proceedingChapter

TY - CHAP

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

AU - Cordy, Maxime

AU - Schobbens, Pierre

AU - Heymans, Patrick

AU - Legay, Axel

PY - 2012/1/1

Y1 - 2012/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84867440812&partnerID=8YFLogxK

U2 - 10.1145/2364412.2364425

DO - 10.1145/2364412.2364425

M3 - Chapter

AN - SCOPUS:84867440812

SN - 9781450310956

VL - 2

SP - 74

EP - 81

BT - ACM International Conference Proceeding Series

ER -