Contributo in atti di convegno, 2017, ENG, 10.1007/978-3-662-54494-5_23

Family-based model checking with mCRL2

Ter Beek M. H.; De Vink E. P.; Willemse T. A.

CNR-ISTI, Pisa, Italy; TU/e Eindhoven, The Netherlands; TU/e Eindhoven, The Netherlands

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.

FASE 2017 - Fundamental Approaches to Software Engineering. 20th International Conference, pp. 387–405, Uppsala, Sweden, 22-29 April 2017

Keywords

(family-based) model checking, mu-calculus (with features), Software Product Lines, Featured Transition Systems

CNR authors

Ter Beek Maurice Henri

CNR institutes

ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"