VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTSv). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTSv or a featured transition system (FTS).

Static analysis and family-based model checking with VMC

ter Beek MH;Mazzanti F;
2021

Abstract

VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTSv). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTSv or a featured transition system (FTS).
2021
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
978-1-4503-8469-8
VMC
SPL
Variability
FTS
MTS
Static analysis
Model checking
File in questo prodotto:
File Dimensione Formato  
prod_456542-doc_176717.pdf

non disponibili

Descrizione: Static analysis and family-based model checking with VMC
Tipologia: Versione Editoriale (PDF)
Dimensione 321.48 kB
Formato Adobe PDF
321.48 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
prod_456542-doc_176718.pdf

accesso aperto

Descrizione: Postprint - Static analysis and family-based model checking with VMC
Tipologia: Versione Editoriale (PDF)
Dimensione 318.09 kB
Formato Adobe PDF
318.09 kB Adobe PDF Visualizza/Apri
prod_456542-doc_176719.pdf

accesso aperto

Descrizione: Preprint - Static analysis and family-based model checking with VMC
Tipologia: Versione Editoriale (PDF)
Dimensione 367.33 kB
Formato Adobe PDF
367.33 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/400108
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact