Cargando…

Statistical Model Checking for Variability-Intensive Systems

We propose a new Statistical Model Checking (SMC) method to discover bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we sample e...

Descripción completa

Detalles Bibliográficos
Autores principales: Cordy, Maxime, Papadakis, Mike, Legay, Axel
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7418118/
http://dx.doi.org/10.1007/978-3-030-45234-6_15
_version_ 1783569629115842560
author Cordy, Maxime
Papadakis, Mike
Legay, Axel
author_facet Cordy, Maxime
Papadakis, Mike
Legay, Axel
author_sort Cordy, Maxime
collection PubMed
description We propose a new Statistical Model Checking (SMC) method to discover bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we sample executions from a featured transition system – a model that represents jointly the state spaces of all variants. The combination of this compact representation and the inherent efficiency of SMC allows us to find bugs much faster (up to 16 times according to our experiments) than other methods. As any simulation-based approach, however, the risk of Type-1 error exists. We provide a lower bound and an upper bound for the number of simulations to perform to achieve the desired level of confidence. Our empirical study involving 59 properties over three case studies reveals that our method manages to discover all variants violating 41 of the properties. This indicates that SMC can act as a low-cost-high-reward method for verifying VIS.
format Online
Article
Text
id pubmed-7418118
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74181182020-08-11 Statistical Model Checking for Variability-Intensive Systems Cordy, Maxime Papadakis, Mike Legay, Axel Fundamental Approaches to Software Engineering Article We propose a new Statistical Model Checking (SMC) method to discover bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we sample executions from a featured transition system – a model that represents jointly the state spaces of all variants. The combination of this compact representation and the inherent efficiency of SMC allows us to find bugs much faster (up to 16 times according to our experiments) than other methods. As any simulation-based approach, however, the risk of Type-1 error exists. We provide a lower bound and an upper bound for the number of simulations to perform to achieve the desired level of confidence. Our empirical study involving 59 properties over three case studies reveals that our method manages to discover all variants violating 41 of the properties. This indicates that SMC can act as a low-cost-high-reward method for verifying VIS. 2020-03-13 /pmc/articles/PMC7418118/ http://dx.doi.org/10.1007/978-3-030-45234-6_15 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Cordy, Maxime
Papadakis, Mike
Legay, Axel
Statistical Model Checking for Variability-Intensive Systems
title Statistical Model Checking for Variability-Intensive Systems
title_full Statistical Model Checking for Variability-Intensive Systems
title_fullStr Statistical Model Checking for Variability-Intensive Systems
title_full_unstemmed Statistical Model Checking for Variability-Intensive Systems
title_short Statistical Model Checking for Variability-Intensive Systems
title_sort statistical model checking for variability-intensive systems
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7418118/
http://dx.doi.org/10.1007/978-3-030-45234-6_15
work_keys_str_mv AT cordymaxime statisticalmodelcheckingforvariabilityintensivesystems
AT papadakismike statisticalmodelcheckingforvariabilityintensivesystems
AT legayaxel statisticalmodelcheckingforvariabilityintensivesystems