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 -