Paper published in a book (Scientific congresses, symposiums and conference proceedings)
Verification of Variability-Intensive Stochastic Systems with Statistical Model Checking
LAZREG, Sami; CORDY, Maxime; Legay, Axel
2022 • In Margaria, Tiziana (Ed.) Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings
Markov chains; Statistical Model Checking; Stochastic systems; Variability; Learn+; LTL formulae; Occurrence probability; Simulation based approaches; Software Product Line; Statistical model checking
Abstract :
[en] We propose a simulation-based approach to verify Variability-Intensive Systems (VISs) with stochastic behaviour. Given an LTL formula and a model of the VIS behaviour, our method estimates the probability for each variant to satisfy the formula. This allows us to learn the products of the VIS for which the probability stands above a certain threshold. To achieve this, our method samples VIS executions from all variants at once and keeps track of the occurrence probability of these executions in any given variant. The efficiency of this algorithm relies on Algebraic Decision Diagram (ADD), a dedicated data structure that enables orthogonal treatment of variability, stochasticity and property satisfaction. We implemented our approach as an extension of the ProVeLines model checker. Our experiments validate that our method can produce accurate estimations of the probability for the variants to satisfy the given properties.
Disciplines :
Computer science
Author, co-author :
LAZREG, Sami ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal
CORDY, Maxime ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SerVal
Legay, Axel; UCLouvain, Louvain-La-Neuve, Belgium
External co-authors :
yes
Language :
English
Title :
Verification of Variability-Intensive Stochastic Systems with Statistical Model Checking
Publication date :
2022
Event name :
Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning: 11th International Symposium, ISoLA 2022
Event place :
Rhodes, Grc
Event date :
22-10-2022 => 30-10-2022
Audience :
International
Main work title :
Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings
Editor :
Margaria, Tiziana
Publisher :
Springer Science and Business Media Deutschland GmbH
FNR Luxembourg C19/IS/13566661/BEEHIVE/Cordy FNR Luxembourg INTER/FNRS/20/15\-077233/Scaling Up Variability/Cordy
Funders :
FNR Luxembourg FNRS Belgium
Funding text :
Maxime Cordy and Sami Lazreg are supported by FNR Luxembourg (grants C19/IS/13566661/BEEHIVE/Cordy and INTER/FNRS/20/15\-077233/Scaling Up Variability/Cordy). Axel Legay is supported by FNRS Belgium (grant PDR/PDN - T013721).
Češka, M., Jansen, N., Junges, S., Katoen, J.-P.: Shepherding Hordes of Markov Chains. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 172– 190. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1 10
Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects of Computing 30(1), 45–75 (2017). https://doi.org/10.1007/s00165-017-0432-4
Classen, A., Cordy, M., Heymans, P., Schobbens, P.Y., Legay, A.: Snip: an efficient model checker for software product lines. Technical report, University of Namur (FUNDP) (2011)
Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. Trans. Softw. Eng. 39, 1069–1089 (2013)
Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: ICSE’10, pp. 335–344. ACM (2010)
Clements, P.C., Northrop, L.: Software Product Lines: Practices and Patterns. SEI Series in Software Engineering, Addison-Wesley (2001)
Cordy, M., Schobbens, P.-Y., Heymans, P., Legay, A.: Provelines: a product-line of verifiers for software product lines. In: SPLC’13, pp. 141–146. ACM (2013)
Daca, P., Henzinger, T.A., Kretínský, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log. 18(2), 12:1– 12:25 (2017)
D’Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of markov decision processes. CoRR, abs/1409.2116 (2014)
Delahaye, B., Fournier, P., Lime, D.: Statistical model checking for parameterized models. working paper or preprint (2019)
Delahaye, B., Fournier, P., Lime, D.: Statistical model checking for parameterized models (2019)
Dubslaff, C., Klüppelholz, S., Baier, C.: Probabilistic model checking for energy analysis in software product lines. In: Binder, W., Ernst, E., Peternier, A., Hirschfeld, R., (eds.) 13th International Conference on Modularity, MODULAR-ITY ’14, Lugano, Switzerland, 22–26 April, 2014, pp. 169–180. ACM (2014)
Gruler, A., Leucker, M., Scheidemann, K.: Modeling and Model Checking Software Product Lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113–131. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68863-1 8
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2004)
Kramer, J., Magee, J., Sloman, M., Lister, A.: Conic: an integrated approach to distributed computer control systems. Comput. Digit. Tech. IEE Proc. E 130(1), 1–10 (1983)
Legay, A., Delahaye, B., Bensalem, S.: Statistical Model Checking: An Overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122– 135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9 11
Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical Model Checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478–504. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91908-9 23
Muschevici, R., Clarke, D., Proenca, J.: Feature petri nets. In: Proceedings of the 14th International Software Product Line Conference (SPLC 2010), vol. 2. Lancaster University, Lancaster, United Kingdom (2010)
Nunes, V., Fernandes, P., Alves, V., Rodrigues, G.: Variability management of reliability models in software product lines: an expressiveness and scalability analysis. In: SBCARS ’12, pp, 51–60 (2012)
Pnueli, A.: The temporal logic of programs. In: FOCS’77, pp. 46–57 (1977)
Raatikainen, M., Soininen, T., Männistö, T., Mattila, A.: A Case Study of Two Configurable Software Product Families. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 403–421. Springer, Heidelberg (2004). https://doi.org/10. 1007/978-3-540-24667-1 30
Rodrigues, G.N., et al.: Modeling and verification for probabilistic properties in software product lines. In: HASE 2015, Daytona Beach, FL, USA, 8–10 January, 2015, pp. 173–180 (2015)
Sabin, D., Weigel, R.: Product configuration frameworks-a survey. IEEE Intell. Syst. Appl. 13(4), 42–49 (1998)
Somenzi, F.: Cudd: Cu Decision Diagram Package-Release 2.4. 0. University of Colorado at Boulder (2012)
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Logical Algebraic Methods Program. 85(2), 287–315 (2016)
ter Beek, M.H., Legay, A., Lluch-Lafuente, A., Vandin, A.: A framework for quantitative modeling and analysis of highly (re)configurable systems. IEEE Trans. Softw. Eng. 46(3), 321–345 (2020)
Vandin, A., ter Beek, M.H., Legay, A., Lluch Lafuente, A.: QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 329– 337. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7 19
Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical Verification of Probabilistic Properties with Unbounded Until. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 144–160. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19829-8 10
Younes, H.L.S., Simmons, R.G.: Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002). https://doi.org/10. 1007/3-540-45657-0 17
