research-article

Run-time efficient probabilistic model checking

Authors:

Antonio Filieri,

Giordano TamburrelliAuthors Info & Claims

ICSE '11: Proceedings of the 33rd International Conference on Software Engineering

Pages 341 - 350

https://doi.org/10.1145/1985793.1985840

Published: 21 May 2011 Publication History

Abstract

Unpredictable changes continuously affect software systems and may have a severe impact on their quality of service, potentially jeopardizing the system's ability to meet the desired requirements. Changes may occur in critical components of the system, clients' operational profiles, requirements, or deployment environments.

The adoption of software models and model checking techniques at run time may support automatic reasoning about such changes, detect harmful configurations, and potentially enable appropriate (self-)reactions. However, traditional model checking techniques and tools may not be simply applied as they are at run time, since they hardly meet the constraints imposed by on-the-fly analysis, in terms of execution time and memory occupation.

This paper precisely addresses this issue and focuses on reliability models, given in terms of Discrete Time Markov Chains, and probabilistic model checking. It develops a mathematical framework for run-time probabilistic model checking that, given a reliability model and a set of requirements, statically generates a set of expressions, which can be efficiently used at run-time to verify system requirements. An experimental comparison of our approach with existing probabilistic model checkers shows its practical applicability in run-time verification.

References

[1]

S. C. Althoen and R. McLaughlin. Gauss-jordan reduction: A brief history. The American Mathematical Monthly, 94(2):130--142, 1987.

Digital Library

[2]

C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.

Digital Library

[3]

L. Baresi and S. Guinea. Towards dynamic monitoring of ws-bpel processes. ICSOC, 2005.

Digital Library

[4]

A. Bojanczyk. Complexity of solving linear systems in different models of computation. SIAM Journal on Numerical Analysis, 21(3):591--603, 1984.

[5]

L. Cheung, R. Roshandel, N. Medvidovic, and L. Golubchik. Early prediction of software component reliability. In ICSE, Leipzig, Germany, May 10-18, 2008, pages 111--120. ACM, 2008.

Digital Library

[6]

R. C. Cheung. A user-oriented software reliability model. IEEE Trans. Softw. Eng., 6(2):118--125, 1980.

Digital Library

[7]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. Springer, 1999.

Digital Library

[8]

D. Coppersmith and S. Winograd. On the asymptotic complexity of matrix multiplication. SIAM J. Comput., 11(3):472--492, 1982.

Digital Library

[9]

V. Cortellessa and V. Grassi. A modeling approach to analyze the impact of error propagation on reliability of component-based systems. In H. W. Schmidt, I. Crnkovic, G. T. Heineman, and J. A. Stafford, editors, CBSE, volume 4608 of LNCS, pages 140--156. Springer, 2007.

Digital Library

[10]

C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4), 1995.

Digital Library

[11]

C. Daws. Symbolic and parametric model checking of discrete-time markov chains. ICTAC, pages 280--294, 2005.

Digital Library

[12]

I. Epifani, C. Ghezzi, R. Mirandola, and G. Tamburrelli. Model evolution by run-time parameter adaptation. In ICSE, 2009.

Digital Library

[13]

A. Filieri, C. Ghezzi, V. Grassi, and R. Mirandola. Reliability analysis of component-based systems with multiple failure modes. In CBSE, pages 1--20, 2010.

Digital Library

[14]

K. Goseva-Popstojanova and K. S. Trivedi. Architecture-based approach to reliability assessment of software systems. Performance Evaluation, 45(2-3):179--204, 2001.

Digital Library

[15]

C. Grinstead and J. Snell. Introduction to Probability. Amer Mathematical Society, 1997.

[16]

E. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric markov models. Model Checking Software, pages 88--106, 2009.

Digital Library

[17]

P. Heidelberger. Fast simulation of rare events in queueing and reliability models. TOMACS, 5(1):43--85, 1995.

Digital Library

[18]

A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. Prism: A tool for automatic verification of probabilistic systems. TACAS, 3920:441--444, 2006.

Digital Library

[19]

A. Immonen and E. Niemela. Survey of reliability and availability prediction methods from the viewpoint of software architecture. Software and Systems Modeling, 7(1):49--65, 2008.

[20]

E. Kaltofen and G. Villard. On the complexity of computing determinants. Computational Complexity, 13(3):91--130, 2005.

Digital Library

[21]

J.-P. Katoen, M. Khattri, and I. S. Zapreev. A Markov reward model checker. In QEST, pages 243--244, Los Alamos, CA, USA, 2005. IEEE Computer Society.

Digital Library

[22]

J.-P. Katoen, I. S. Zapreev, E. M. Hahn, H. Hermanns, and D. N. Jansen. The ins and outs of the probabilistic model checker mrmc. Performance Evaluation, In Press, Corrected Proof:-, 2010.

Digital Library

[23]

M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. Formal Methods for Performance Evaluation, pages 220--270.

Digital Library

[24]

M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. In T. Field, P. Harrison, J. Bradley, and U. Harder, editors, Computer Performance Evaluation: Modelling Techniques and Tools, volume 2324 of Lecture Notes in Computer Science, pages 113--140. Springer Berlin / Heidelberg, 2002.

Digital Library

[25]

K. W. Miller, L. J. Morell, R. E. Noonan, S. K. Park, D. M. Nicol, B. W. Murrill, and J. M. Voas. Estimating the probability of failure when testing reveals no failures. IEEE Trans. Softw. Eng., 18(1):33--43, 1992.

Digital Library

[26]

C. Rahmani, H. Siy, and A. Azadmanesh. An experimental analysis of open source software reliability. In F2DA, Niagara Falls, 2009.

[27]

S. Ross. Stochastic Processes. Wiley New York, 1996.

[28]

J. Zhang and B. H. C. Cheng. Model-based development of dynamically adaptive software. In ICSE, pages 371--380. ACM, 2006.

Digital Library

[29]

T. Zheng, M. Woodside, and M. Litoiu. Performance model estimation and tracking using optimal filters. IEEE Trans. Softw. Eng., 34(3):391--406, 2008.

Digital Library

Cited By

Göttmann HCaesar BBeers LLochau MSchürr AFay A(2024)Cost-sensitive precomputation of real-time-aware reconfiguration strategies based on stochastic priced timed gamesSoftware and Systems Modeling10.1007/s10270-024-01195-9Online publication date: 5-Aug-2024
https://doi.org/10.1007/s10270-024-01195-9
Xu HSchneider SGiese H(2024)Combining Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation SystemsFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_4(77-100)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57259-3_4
Fang XYaman SCalinescu RWilson JPaterson C(2023)Predicting Nonfunctional Requirement Violations in Autonomous SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/3632405Online publication date: 14-Nov-2023
https://dl.acm.org/doi/10.1145/3632405
Show More Cited By

Index Terms

Run-time efficient probabilistic model checking

Recommendations

Model checking epistemic-probabilistic logic using probabilistic interpreted systems

Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. ...
On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination

We show a new procedure combining on-the-fly model-checking and mean-field.We prove the asymptotic correctness of the on-the-fly model-checking procedure.We present a prototype implementation of the model-checking.We use the technique to analyze ...
Efficient Java exception handling in just-in-time compilation
Research Articles

Java uses exceptions to provide elegant error handling capabilities during program execution. However, the presence of exception handlers complicates the job of the just-in-time (JIT) compiler, while exceptions are rarely used in most programs. This ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '11: Proceedings of the 33rd International Conference on Software Engineering

May 2011

1258 pages

ISBN:9781450304450

DOI:10.1145/1985793

General Chair:
Richard N. Taylor
UC Irvine, USA
,
Program Chairs:
Harald Gall
University of Zurich, Switzerland
,
Nenad Medvidović
University of Southern California, USA

Copyright © 2011 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 May 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSE11

Sponsor:

SIGSOFT

ICSE11: International Conference on Software Engineering

May 21 - 28, 2011

HI, Waikiki, Honolulu, USA

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

135
Total Citations
View Citations
1,218
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)0

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Göttmann HCaesar BBeers LLochau MSchürr AFay A(2024)Cost-sensitive precomputation of real-time-aware reconfiguration strategies based on stochastic priced timed gamesSoftware and Systems Modeling10.1007/s10270-024-01195-9Online publication date: 5-Aug-2024
https://doi.org/10.1007/s10270-024-01195-9
Xu HSchneider SGiese H(2024)Combining Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation SystemsFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_4(77-100)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57259-3_4
Fang XYaman SCalinescu RWilson JPaterson C(2023)Predicting Nonfunctional Requirement Violations in Autonomous SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/3632405Online publication date: 14-Nov-2023
https://dl.acm.org/doi/10.1145/3632405
Fang XCalinescu RGerasimou SAlhwikem F(2023)Fast Parametric Model Checking With Applications to Software Performability AnalysisIEEE Transactions on Software Engineering10.1109/TSE.2023.331364549:10(4707-4730)Online publication date: 1-Oct-2023
https://doi.org/10.1109/TSE.2023.3313645
Carwehl MVogel TRodrigues GGrunske L(2023)Runtime Verification of Self-Adaptive Systems with Changing Requirements2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS)10.1109/SEAMS59076.2023.00024(104-114)Online publication date: May-2023
https://doi.org/10.1109/SEAMS59076.2023.00024
Agos Jawaddi SIsmail AMohammad Hatta MKamarulzaman A(2023)Insights into cloud autoscaling: a unique perspective through MDP and DTMC formal modelsThe Journal of Supercomputing10.1007/s11227-023-05665-780:4(5073-5107)Online publication date: 23-Sep-2023
https://doi.org/10.1007/s11227-023-05665-7
Korn MChrszon PKlüppelholz SBaier CWunderlich S(2023)Effectiveness of Pre-computed Knowledge in Self-adaptation - A Robustness StudyComputer Performance Engineering10.1007/978-3-031-25049-1_2(19-34)Online publication date: 25-Jan-2023
https://doi.org/10.1007/978-3-031-25049-1_2
Göttmann HCaesar BBeers LLochau MSchürr AFay ASyriani ESahraoui H(2022)Precomputing reconfiguration strategies based on stochastic timed game automataProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems10.1145/3550355.3552397(31-42)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550355.3552397
El-Rewini ZZhang ZAafer YYin HStavrou ACremers CShi E(2022)PoirotProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security10.1145/3548606.3560710(937-950)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3548606.3560710
Weyns DGheibi OQuin FVan Der Donckt J(2022)Deep Learning for Effective and Efficient Reduction of Large Adaptation Spaces in Self-adaptive SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/353019217:1-2(1-42)Online publication date: 29-Jul-2022
https://dl.acm.org/doi/10.1145/3530192
Show More Cited By

View Options

Get Access

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