Abstract
This short paper summarises the contributions published in [4], where we introduce QFLan, a framework for quantitative modeling and analysis of highly (re)configurable systems, like software product lines. We define a rich domain specific language (DSL) for systems with variability in terms of features, which can be dynamically installed, removed or replaced, capable of modeling probabilistic behavior, possibly subject to quantitative feature constraints. High-level DSL specifications are automatically encoded in a process algebra whose operational behavior interacts with a store of constraints, which allows to separate a system’s configuration from its behavior. The resulting probabilistic configurations and behavior converge seamlessly in a semantics based on discrete-time Markov chains, thus enabling quantitative analysis. An accompanying Eclipse-based tool offers a modern integrated development environment to specify such systems and to perform analyses that range from the likelihood of specific behavior to the expected average cost, in terms of feature attributes, of specific system variants. Based on a seamless integration with the statistical model checker MultiVeStA, QFLan allows to scale to larger models with respect to precise probabilistic analysis techniques. We provide a number of case studies that have driven and validated the development of the QFLan framework. In particular, we show the versatility of the QFLan framework with an application to risk analysis of a safe lock system from the security domain.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Quantitative analysis of probabilistic models of software product lines with statistical model checking. EPTCS 182, 56–70 (2015). https://doi.org/10.4204/EPTCS.182.5
ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: SPLC, pp. 11–15. ACM (2015). https://doi.org/10.1145/2791060.2791087
ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114–133. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_8
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. (2018). https://doi.org/10.1109/TSE.2018.2853726
Schneier, B.: Attack trees. Dr. Dobb’s J. 24(12), 21–29 (1999)
Schneier, B.: Secrets & Lies: Digital Security in a Networked World. Wiley, New York (2000)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A. (2019). Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_35
Download citation
DOI: https://doi.org/10.1007/978-3-030-34968-4_35
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-34967-7
Online ISBN: 978-3-030-34968-4
eBook Packages: Computer ScienceComputer Science (R0)