Book chapter · Conference paper
Statistical Model Checking for Product Lines
National Research Council of Italy1
French National Institute for Computer Science and Applied Mathematics2
Department of Applied Mathematics and Computer Science, Technical University of Denmark3
Formal Methods, Department of Applied Mathematics and Computer Science, Technical University of Denmark4
IMT Institute for Advanced Studies Lucca5
We report on the suitability of statistical model checking for the analysis of quantitative properties of product line models by an extended treatment of earlier work by the authors. The type of analysis that can be performed includes the likelihood of specific product behaviour, the expected average cost of products (in terms of the attributes of the products’ features) and the probability of features to be (un)installed at runtime.
The product lines must be modelled in QFLan, which extends the probabilistic feature-oriented language PFLan with novel quantitative constraints among features and on behaviour and with advanced feature installation options. QFLan is a rich process-algebraic specification language whose operational behaviour interacts with a store of constraints, neatly separating product configuration from product behaviour.
The resulting probabilistic configurations and probabilistic behaviour converge in a discrete-time Markov chain semantics, enabling the analysis of quantitative properties. Technically, a Maude implementation of QFLan, integrated with Microsoft’s SMT constraint solver Z3, is combined with the distributed statistical model checker MultiVeStA, developed by one of the authors.
We illustrate the feasibility of our framework by applying it to a case study of a product line of bikes.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2016 |
Pages: | 114-33 |
Proceedings: | 7<sup>th</sup> International Symposium on Leveraging Applications of Formal Methods, Verification and Validation |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | 7th International Symposium, Isola 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I |
ISBN: | 3319471651 , 331947166X , 331947166x , 9783319471655 and 9783319471662 |
ISSN: | 16113349 and 03029743 |
Types: | Book chapter and Conference paper |
DOI: | 10.1007/978-3-319-47166-2_8 |
ORCIDs: | Lluch Lafuente, Alberto |
Artificial intelligence (incl. robotics) Computation by abstract devices Logics and meanings of programs Mathematical logic and formal languages Programming languages, compilers, interpreters Software engineering techniques
Action Constraint Artificial Intelligence (incl. Robotics) Computation by Abstract Devices Computer Science Label Transition System Logics and Meanings of Programs Mathematical Logic and Formal Languages Model Check Product Line Programming Languages, Compilers, Interpreters Software Engineering Software Product Line