More Web Proxy on the site http://driver.im/

research-article

Discrete time Markov chain families: modeling and verification of probabilistic software product lines

Authors:

Mahsa Varshosaz,

Ramtin KhosraviAuthors Info & Claims

SPLC '13 Workshops: Proceedings of the 17th International Software Product Line Conference co-located workshops

Pages 34 - 41

https://doi.org/10.1145/2499777.2500725

Published: 26 August 2013 Publication History

Abstract

Software product line engineering (SPLE) enables systematic reuse in development of a family of related software systems by explicitly defining commonalities and variabilities among the individual products in the family. Nowadays, SPLE is used in a variety of complex domains such as avionics and automotive. As such domains include safety critical systems which exhibit probabilistic behavior, there is a major need for modeling and verification approaches dealing with probabilistic aspects of systems in the presence of variabilities. In this paper, we introduce a mathematical model, Discrete Time Markov Chain Family (DTMCF), which compactly represents the probabilistic behavior of all the products in the product line. We also provide a probabilistic model checking method to verify DTMCFs against Probabilistic Computation Tree Logic (PCTL) properties. This way, instead of verifying each product individually, the whole family is model checked at once, resulting in the set of products satisfying the desired property. This reduces the required cost for model checking by eliminating redundant processing caused by the commonalities among the products.

References

[1]

C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008.

Digital Library

[2]

D. Batory. Feature models, grammars, and propositional formulas. In Proc. of the 9th intl. conference on Software Product Lines, SPLC'05, pages 7--20, Berlin, Heidelberg, 2005. Springer-Verlag.

Digital Library

[3]

D. Benavides, S. Segura, and A. Ruiz-Cortés. Automated analysis of feature models 20 years later: A literature review. volume 35, pages 615--636, Oxford, UK, UK, Sept. 2010. Elsevier Science Ltd.

Digital Library

[4]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677--691, Aug. 1986.

Digital Library

[5]

E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999.

Digital Library

[6]

A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin. Featured transition systems: Foundations for verifying variability-intensive systems and their application to ltl model checking. IEEE Transactions on Software Engineering, 99(PrePrints):1, 2013.

Digital Library

[7]

A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic model checking of software product lines. In Proc. of the 33rd Inl. Conference on Software Engineering, ICSE '11, pages 321--330, New York, NY, USA, 2011. ACM.

Digital Library

[8]

A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model checking lots of systems: efficient verification of temporal properties in software product lines. In Proc. of the 32nd ACM/IEEE Intl. Conference on Software Engineering - Volume 1, ICSE '10, pages 335--344, New York, NY, USA, 2010. ACM.

Digital Library

[9]

M. Cordy, P.-Y. Schobbens, P. Heymans, and A. Legay. Behavioural modelling and verification of real-time software product lines. In Proc. of the 16th Intl. Software Product Line Conference - Volume 1, SPLC '12, pages 66--75, New York, USA, 2012. ACM.

Digital Library

[10]

V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker. Automated verification techniques for probabilistic systems. In M. Bernardo and V. Issarny, editors, Formal Methods for Eternal Networked Software Systems (SFM'11), volume 6659 of LNCS, pages 53--113. Springer, 2011.

[11]

C. Ghezzi and A. Molzam Sharifloo. Quantitative Verification of Non-Functional Requirements with Uncertainty. In Sixth Intl. Conference on Dependability and Computer Systems, pages 47--62. Springer, 2011.

[12]

C. Ghezzi and A. M. Sharifloo. Verifying non-functional properties of software product lines: Towards an efficient approach using parametric model checking. In Proc. of the 15th Intl. Software Product Line Conference, SPLC '11, pages 170--174, Washington, DC, USA, 2011. IEEE Computer Society.

Digital Library

[13]

E. Goldberg and Y. Novikov. Berkmin: A fast and robust sat-solver. Discrete Appl. Math., 155(12):1549--1561, June 2007.

Digital Library

[14]

R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics: A Foundation for Computer Science. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2nd edition, 1994.

Digital Library

[15]

E. M. Hahn. Parametric markov model analysis. Master's thesis, Saarland University, Germany, 2008.

[16]

E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. Param: a model checker for parametric markov models. In Proc. of the 22nd intl. conference on Computer Aided Verification, CAV'10, pages 660--664, Berlin, Heidelberg, 2010. Springer-Verlag.

Digital Library

[17]

H. Hansson and B. Jonsson. A framework for reasoning about time and reliability. In IEEE Real-Time Systems Symposium, pages 102--111, 1989.

[18]

K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson. Feature-Oriented Domain Analysis (FODA) Feasibility Study. Technical Report CMU/SEI-90-TR-21, Software Engineering Institute, Carnegie Mellon University, 1990.

[19]

M. Kwiatkowska and D. Parker. Advances in probabilistic model checking. In T. Nipkow, O. Grumberg, and B. Hauptmann, editors, Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 126--151. IOS Press, 2012.

[20]

V. Nunes, P. Fernandes, V. Alves, and G. N. Rodrigues. Variability management of reliability models in software product lines: An expressiveness and scalability analysis. In SBCARS, pages 51--60, 2012.

Digital Library

[21]

M. Plath and M. Ryan. Feature integration using a feature construct. Science of Computer Programming, 41(1):53--84, 2001.

Digital Library

[22]

K. Pohl, G. Böckle, and F. J. v. d. Linden. Software Product Line Engineering: Foundations, Principles and Techniques. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2005.

Digital Library

[23]

H. Sabouri, M. M. Jaghoori, F. d. Boer, and R. Khosravi. Scheduling and analysis of real-time software families. In Proc. of the 2012 IEEE 36th Annual Computer Software and Applications Conference, COMPSAC '12, pages 680--689, Washington, DC, USA, 2012. IEEE Computer Society.

Digital Library

[24]

A. von Rhein, S. Apel, C. Kästner, T. Thüm, and I. Schaefer. The pla model: on the combination of product-line analyses. In Proc. of the Seventh Intl. Workshop on Variability Modelling of Software-intensive Systems, VaMoS '13, pages 14:1--14:8, New York, NY, USA, 2013. ACM.

Digital Library

[25]

H. Zhang. Sato: An efficient propositional prover. In Proc. of the 14th Intl. Conference on Automated Deduction, CADE '14, pages 272--275, London, UK, 1997. Springer-Verlag.

Digital Library

Cited By

Kishi T(2023)Family-based Model Checking using Probabilistic Model Checker PRISM2023 30th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC60848.2023.00048(376-385)Online publication date: 4-Dec-2023
https://doi.org/10.1109/APSEC60848.2023.00048
Damasceno CMousavi MSimao A(2021)Learning by sampling: learning behavioral family models from software product linesEmpirical Software Engineering10.1007/s10664-020-09912-w26:1Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1007/s10664-020-09912-w
Thüm TLopez-Herrejon R(2020)A BDD for Linux?Proceedings of the 24th ACM Conference on Systems and Software Product Line: Volume A - Volume A10.1145/3382025.3414943(1-6)Online publication date: 19-Oct-2020
https://dl.acm.org/doi/10.1145/3382025.3414943
Show More Cited By

Index Terms

Discrete time Markov chain families: modeling and verification of probabilistic software product lines
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Model Checking of Software Product Lines in Presence of Nondeterminism and Probabilities
APSEC '14: Proceedings of the 2014 21st Asia-Pacific Software Engineering Conference - Volume 01

Nowadays, Software Product Lines (SPLs) are being used in a variety of domains including safety-critical systems for which verification of the systems is a matter of concern. Formal modeling and verification of SPLs has been majorly investigated ...
Software Configuration Management for Product Derivation in Software Product Families
ECBS '08: Proceedings of the 15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems

A key process in software product line (SPL) engineering is product derivation, which is the process of building software products from a base set of core assets. During product derivation, the components in both core assets and derived software ...
Development and configuration of service-oriented systems families
SAC '11: Proceedings of the 2011 ACM Symposium on Applied Computing

Software Product Lines (SPLs) are families of software systems which share a common sets of feature and are developed through common set of core assets in order to promotes software reusability, mass customization, reducing cost, time-to-market and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SPLC '13 Workshops: Proceedings of the 17th International Software Product Line Conference co-located workshops

August 2013

148 pages

ISBN:9781450323253

DOI:10.1145/2499777

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 August 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLC 2013 workshops

SPLC 2013 workshops: 17th International Software Product Line Conference co-located workshops

August 26 - 30, 2013

Tokyo, Japan

Acceptance Rates

Overall Acceptance Rate 167 of 463 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
190
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)2

Reflects downloads up to 22 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kishi T(2023)Family-based Model Checking using Probabilistic Model Checker PRISM2023 30th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC60848.2023.00048(376-385)Online publication date: 4-Dec-2023
https://doi.org/10.1109/APSEC60848.2023.00048
Damasceno CMousavi MSimao A(2021)Learning by sampling: learning behavioral family models from software product linesEmpirical Software Engineering10.1007/s10664-020-09912-w26:1Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1007/s10664-020-09912-w
Thüm TLopez-Herrejon R(2020)A BDD for Linux?Proceedings of the 24th ACM Conference on Systems and Software Product Line: Volume A - Volume A10.1145/3382025.3414943(1-6)Online publication date: 19-Oct-2020
https://dl.acm.org/doi/10.1145/3382025.3414943
Ebnauf MAbdelmoez WAmmar HHassan AAbdelhamid M(2019)State-driven Architecture Design for Safety-critical Software Product Lines2019 7th International Conference on Mechatronics Engineering (ICOM)10.1109/ICOM47790.2019.8952006(1-6)Online publication date: Oct-2019
https://doi.org/10.1109/ICOM47790.2019.8952006
Češka MHensel CJunges SKatoen J(2019)Counterexample-Driven Synthesis for Probabilistic Program SketchesFormal Methods – The Next 30 Years10.1007/978-3-030-30942-8_8(101-120)Online publication date: 23-Sep-2019
https://doi.org/10.1007/978-3-030-30942-8_8
Češka MJansen NJunges SKatoen J(2019)Shepherding Hordes of Markov ChainsAdvances in Knowledge Discovery and Data Mining10.1007/978-3-030-17465-1_10(172-190)Online publication date: 3-Apr-2019
https://doi.org/10.1007/978-3-030-17465-1_10
Beek MVink EWillemse T(2017)Family-Based Model Checking with mCRL2Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering - Volume 1020210.1007/978-3-662-54494-5_23(387-405)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54494-5_23
Santos IRocha LNeto PAndrade R(2016)Model Verification of Dynamic Software Product LinesProceedings of the XXX Brazilian Symposium on Software Engineering10.1145/2973839.2973852(113-122)Online publication date: 19-Sep-2016
https://dl.acm.org/doi/10.1145/2973839.2973852
ter Beek MLegay ALluch Lafuente AVandin A(2016)Statistical Model Checking for Product LinesLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques10.1007/978-3-319-47166-2_8(114-133)Online publication date: 5-Oct-2016
https://doi.org/10.1007/978-3-319-47166-2_8
ter Beek MLegay ALluch Lafuente AVandin A(2015)Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model CheckingElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.182.5182(56-70)Online publication date: 12-Apr-2015
https://doi.org/10.4204/EPTCS.182.5
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents