Name
Abstract | ||
|---|---|---|
We consider the problem of model checking Variability-Intensive Systems (VIS) against non-functional requirements. These requirements are typically expressed as an optimization problem over quality attributes of interest, whose value is determined by the executions of the system. Identifying the optimal variant can be hard due to the state-explosion problem inherent to model checking the exponentially growing number of variants in large VIS. In this paper, we lay the foundations for the application of smart sampling and statistical model checking to solve this problem faster. We design a simple method that samples variants and executions in a uniform manner from a featured weighted automaton and that assesses which of the sampled variants/executions are optimal. We implemented our approach on top of ProVeLines, a tool suite for model-checking VIS and carried out a preliminary evaluation on an industrial embedded system design case study. Our results show that sampling-based approaches indeed holds the potential to improve scalability but should be supported by better heuristics to be competitive.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1109/FormaliSE.2019.00015 | Proceedings of the 7th International Workshop on Formal Methods in Software Engineering |
Keywords | DocType | ISSN |
model checking, sampling, variability | Conference | 2380-873X |
ISBN | Citations | PageRank |
978-1-7281-3374-4 | 1 | 0.35 |
References | Authors | |
11 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maxime Cordy | 1 | 464 | 30.81 |
| Axel Legay | 2 | 2982 | 181.47 |
| Sami Lazreg | 3 | 3 | 1.73 |
| Philippe Collet | 4 | 652 | 49.32 |