Towards a feature mu-calculus targeting SPL verification

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

8 Citaten (Scopus)
83 Downloads (Pure)


The modal μ-calculus μL is a well-known fixpoint logic to express and model check properties interpreted over labeled transition systems. In this paper, we propose two variants of the μ-calculus, μLf and μL?f, for feature transition systems. For this, we explicitly incorporate feature expressions into the logics, allowing operators to select transitions and behavior restricted to specific products and subfamilies. We provide semantics for μLf and μL?f and relate the two new μ-calculi and μL to each other. Next, we focus on the analysis of SPL behavior and show how our formalism can be applied for product-based verification with μLf as well as family-based verification with μL?f. We illustrate by means of a toy example how properties can be model checked, exploiting an embedding of μL?f into the μ-calculus with data.

Originele taal-2Engels
Pagina's (van-tot)61-75
Aantal pagina's15
TijdschriftElectronic Proceedings in Theoretical Computer Science, EPTCS
StatusGepubliceerd - 28 mrt 2016
Evenement7th International Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE’16) - Eindhoven, Nederland
Duur: 3 apr 20163 apr 2016


Duik in de onderzoeksthema's van 'Towards a feature mu-calculus targeting SPL verification'. Samen vormen ze een unieke vingerafdruk.

Citeer dit