Back to Search
Start Over
Static analysis and family-based model checking of featured transition systems with VMC
- Source :
- SPLC (B), SPLC'21-25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021, info:cnr-pdr/source/autori:ter Beek M.H.; Mazzanti F.; Damiani F.; Paolini L.; Scarso G.; Valfrè M.; Lienhardt M./congresso_nome:SPLC'21-25th ACM International Systems and Software Product Line Conference/congresso_luogo:Leicester, UK/congresso_data:06-10%2F09%2F2021/anno:2021/pagina_da:24/pagina_a:27/intervallo_pagine:24–27
- Publication Year :
- 2021
- Publisher :
- ACM, 2021.
-
Abstract
- A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.
- Subjects :
- Model checking
SPL
Theoretical computer science
Computer science
MTS
Toolchain
software product lines
Feature (machine learning)
tool support
Variability
Formal verification
VMC
formal verification
FTS
static analysis
variability
Deadlock
Static analysis
model checking
featured transition systems
configurable systems
Transition system
modal transition systems
State (computer science)
variability models
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- Proceedings of the 25th ACM International Systems and Software Product Line Conference - Volume B
- Accession number :
- edsair.doi.dedup.....c2962abda4c9ab35f83e444467805007