Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., De Vink E. P., Willemse T. A. Family-based model checking with mCRL2. In: FASE 2017 - Fundamental Approaches to Software Engineering. 20th International Conference (Uppsala, Sweden, 22-29 April 2017). Proceedings, vol. 10202 pp. 387 - 405. Marieke Huisman, Julia Rubin (eds.). (Lecture Notes in Computer Science, vol. 10202). Springer, 2017.
Family-based model checking targets the simultaneous verification of multiple system variants, a technique to handle feature-based variability that is intrinsic to software product lines (SPLs). We present an approach for family-based verification based on the feature mu-calculus mu-Lf, which combines modalities with feature expressions. This logic is interpreted over featured transition systems, a well-accepted model of SPLs, which allows one to reason over the collective behavior of a number of variants (a family of products). Via an embedding into the modal mu-calculus with data, underpinned by the general-purpose mCRL2 toolset, off-the-shelf tool support for mu-Lf becomes readily available. We illustrate the feasibility of our approach on an SPL benchmark model and show the runtime improvement that family-based model checking with mCRL2 offers with respect to model checking the benchmark product-by-product.
URL: http://link.springer.com/chapter/10.1007%2F978-3-662-54494-5_23
DOI: 10.1007/978-3-662-54494-5_23
Subject (family-based) model checking
mu-calculus (with features)
Software Product Lines
Featured Transition Systems
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Formal methods
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Model checking
D.2.13 SOFTWARE ENGINEERING. Reusable Software. Domain engineering

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional