Towards sampling and simulation-based analysis of featured weighted automata
Pages 61 - 64
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.
References
[1]
P. C. Clements and L. Northrop, Software Product Lines: Practices and Patterns, ser. SEI Series in Software Engineering. Addison-Wesley, August 2001.
[2]
A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. cois Raskin, "Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking," Transactions on Software Engineering, pp. 1069--1089, 2013.
[3]
M. H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti, "Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints," Journal of Logical and Algebraic Methods in Programming, vol. 85, no. 2, pp. 287 -- 315, 2016.
[4]
M. Chechik, B. Devereux, S. M. Easterbrook, and A. Gurfinkel, "Multi-valued symbolic model-checking," ACM Trans. Softw. Eng. Methodol., vol. 12, no. 4, pp. 371--408, 2003.
[5]
K. Lauenroth, S. Toehning, and K. Pohl, "Model checking of domain artifacts in product line engineering," in IEEE/ACM ASE, 2009, pp. 269--280.
[6]
M. Cordy, P. Heymans, P.-Y. Schobbens, and A. Legay, "Behavioural modelling and verification of real-time software product lines," in SPLC'12. ACM, 2012.
[7]
G. N. Rodrigues, V. Alves, V. Nunes, A. Lanna, M. Cordy, P. Schobbens, A. M. Sharifloo, and A. Legay, "Modeling and verification for probabilistic properties in software product lines," in HASSE 2015, Daytona Beach, FL, USA, January 8--10, 2015, 2015, pp. 173--180.
[8]
R. Olaechea, U. Fahrenberg, J. M. Atlee, and A. Legay, "Long-term average cost in featured transition systems," in Proceedings of the 20th International Systems and Software Product Line Conference, ser. SPLC '16. New York, NY, USA: ACM, 2016, pp. 109--118. {Online}. Available
[9]
S. Lazreg, P. Collet, and S. Mosser, "Assessing the functional feasibility of variability-intensive data flow-oriented systems," in .Symposium on Applied Computing, 2018.
[10]
U. Fahrenberg and A. Legay, "Featured weighted automata," in FormaliSE@ICSE 2017, 2017, pp. 51--57.
[11]
S. Lazreg, M. Cordy, P. Collet, P. Heymans, and S. Mosser, "Multi-faceted automated analyses for variability-intensive embedded systems," in ICSE '19 (to appear), 2019.
[12]
S. Lazreg, P. Collet, and S. Mosser, "Functional feasibility analysis of variability-intensive data flow-oriented applications over highly-configurable platforms," ACM SIGAPP Applied Computing Review, vol. 18, no. 3, pp. 32--48, 2018.
[13]
A. Legay, B. Delahaye, and S. Bensalem, "Statistical model checking: An overview," in Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1--4, 2010. Proceedings, 2010, pp. 122--135.
[14]
A. David, K. G. Larsen, A. Legay, M. Mikucionis, and D. B. Poulsen, "Uppaal SMC tutorial," STTT, vol. 17, no. 4, pp. 397--415, 2015.
[15]
A. Legay, S. Sedwards, and L. Traonouez, "Estimating rewards & rare events in nondeterministic systems," ECEASST, vol. 72, 2015. {Online}. Available
[16]
F. Medeiros, C. Kästner, M. Ribeiro, R. Gheyi, and S. Apel, "A comparison of 10 sampling algorithms for configurable systems," in ICSE'16.
[17]
M. Varshosaz, M. Al-Hajjaji, T. Thüm, T. Runge, M. R. Mousavi, and I. Schaefer, "A classification of product sampling for software product lines," in SPLC '18, 2018, pp. 1--13.
[18]
Q. Plazar, M. Acher, G. Perrouin, X. Devroey, and M. Cordy, "Uniform sampling of sat solutions for configurable systems: Are we there yet?" in ICST '19 (to appear), 2019.
[19]
M. Cordy, P.-Y. Schobbens, P. Heymans, and A. Legay, "Provelines: A product-line of verifiers for software product lines," in SPLC'13. ACM, 2013, pp. 141--146.
Recommendations
Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking
The premise of variability-intensive systems, specifically in software product line engineering, is the ability to produce a large family of different systems efficiently. Many such systems are critical. Thorough quality assurance techniques are thus ...
Software product line analysis with mCRL2
SPLC '14: Proceedings of the 18th International Software Product Line Conference: Companion Volume for Workshops, Demonstrations and Tools - Volume 2The mCRL2 language and supporting software provide a state-of-the-art tool suite for the verification of distributed systems. In this paper, we present the general principles, extrapolated from [7,8], which make us believe that mCRL2 can also be used ...
Model Checking of Domain Artifacts in Product Line Engineering
ASE '09: Proceedings of the 24th IEEE/ACM International Conference on Automated Software EngineeringIn product line engineering individual products are derived from the domain artifacts of the product line. The reuse of the domain artifacts is constraint by the product line variability. Since domain artifacts are reused in several products, product ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- SIGSOFT: ACM Special Interest Group on Software Engineering
- IEEE-CS: Computer Society
Publisher
IEEE Press
Publication History
Published: 27 May 2019
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ICSE '19
Sponsor:
- SIGSOFT
- IEEE-CS
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 26Total Downloads
- Downloads (Last 12 months)3
- Downloads (Last 6 weeks)0
Reflects downloads up to 24 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in