research-article

Advanced features in SMART: the stochastic model checking analyzer for reliability and timing

Authors:

Gianfranco Ciardo,

Andrew S. Miner,

Min WanAuthors Info & Claims

ACM SIGMETRICS Performance Evaluation Review, Volume 36, Issue 4

Pages 58 - 63

https://doi.org/10.1145/1530873.1530885

Published: 25 March 2009 Publication History

Abstract

We describe some of the advanced features of the software tool SmArT, the Stochastic Model checking Analyzer for Reliability and Timing. Initially conceived as a software package for numerical solution and discrete-event simulation of stochastic models, SmArT now also provides powerful modelchecking capabilities, thanks to its extensive use of various forms of decision diagrams, which in turn also greatly increase the efficiency of its stochastic analysis algorithms. These aspects make it an excellent choice when tackling systems with extremely large state spaces.

References

[1]

M. Ajmone Marsan and G. Chiola. On Petri nets with deterministic and exponentially distributed firing times. In Adv. in Petri Nets 1987, LNCS 266, pages 132--145. Springer-Verlag, 1987.

Digital Library

[2]

A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS, pages 193--207. Springer-Verlag, 1999.

Digital Library

[3]

P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp., 12(3):203--222, 2000.

[4]

H. Choi, V.G. Kulkarni, and K.S. Trivedi. Markov regenerative stochastic Petri nets. In Performance '93. North-Holland, Sept. 1993.

Digital Library

[5]

G. Ciardo. Data representation and efficient solution: a decision diagram approach. In Formal Methods for Performance Evaluation, LNCS 4486, pages 371--394, May 2007. Springer-Verlag.

Digital Library

[6]

G. Ciardo, R. German, and C. Lindemann. A characterization of the stochastic process underlying a stochastic Petri net. IEEE Trans. Softw. Eng., 20(7):506--515, July 1994.

Digital Library

[7]

G. Ciardo and C. Lindemann. Analysis of deterministic and stochastic Petri nets. In Proc. PNPM, pages 160--169, Oct. 1993. IEEE CS Press.

[8]

G. Ciardo, G. Lüttgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state space generation. In Proc. TACAS, LNCS 2031, pages 328--342, Apr. 2001. Springer-Verlag.

Digital Library

[9]

G. Ciardo, R. Marmorstein, and R. Siminiceanu. The saturation algorithm for symbolic state space exploration. Software Tools for Technology Transfer, 8(1):4--25, Feb. 2006.

[10]

G. Ciardo and A.S. Miner. A data structure for the efficient Kronecker solution of GSPNs. In Proc. PNPM, pages 22--31, Sept. 1999. IEEE CS Press.

Digital Library

[11]

G. Ciardo, A.S. Miner, M. Wan, and A.J. Yu. Approximating stationary measures of structured continuous-time Markov models using matrix diagrams. ACM SIGMETRICS Perf. Eval. Rev., 35(3):16--18, Dec. 2007.

Digital Library

[12]

G. Ciardo and R. Siminiceanu. Structural symbolic CTL model checking of asynchronous systems. In Proc. CAV, LNCS 2725, pages 40--53, July 2003. Springer-Verlag.

[13]

G. Ciardo and A.J. Yu. Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In Proc. CHARME, LNCS 3725, pages 146--161, Oct. 2005. Springer-Verlag.

Digital Library

[14]

E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 1999.

Digital Library

[15]

P. Fernandes, B. Plateau, and W.J. Stewart. Efficient descriptor-vector multiplication in stochastic automata networks. J. ACM, 45(3):381--414, 1998.

Digital Library

[16]

R.L. Jones and G. Ciardo. On phased delay stochastic Petri nets: Definition and an application. In Proc. PNPM, pages 165--174, Sept. 2001. IEEE CS Press.

Digital Library

[17]

R.L. Jones and G. Ciardo. Regenerative simulation of stochastic Petri nets with discrete and continuous timing. In Proc. PMCCS, pages 23--26, Sept. 2003.

[18]

A.S. Miner. Efficient solution of GSPNs using canonical matrix diagrams. In Proc. PNPM, pages 101--110, Sept. 2001. IEEE CS Press.

Digital Library

[19]

A.S. Miner, G. Ciardo, and S. Donatelli. Using the exact state space of a Markov model to compute approximate stationary measures. In Proc. SIGMETRICS, pages 207--216, June 2000. ACM Press.

Digital Library

[20]

A.S. Miner and D. Parker. Symbolic representations and analysis of large state spaces. In Validation of Stochastic Systems, LNCS 2925, pages 296--338. Springer-Verlag, 2004.

[21]

B. Plateau. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In Proc. SIGMETRICS, pages 147--153, May 1985.

Digital Library

[22]

W.J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.

[23]

M. Wan and G. Ciardo. Extensible decision diagrams for symbolic state-space generation of asynchronous systems. In Proc. SOFSEM, Jan. 2009. Springer-Verlag. To appear.

Digital Library

[24]

M. Wan and G. Ciardo. Symbolic reachability analysis of integer timed Petri nets. In Proc. SOFSEM, Jan. 2009. Springer-Verlag. To appear.

Digital Library

[25]

M. Wan, G. Ciardo, and A.S. Miner. Decision-diagram-based approximate steady-state analysis of large structured Markov models. In preparation.

[26]

A.J. Yu, G. Ciardo, and G. Lüttgen. Bounded reachability checking of asynchronous systems using decision diagrams. In Proc. TACAS, LNCS 4424, pages 648--663, Mar. 2007. Springer-Verlag.

Digital Library

Cited By

Sølvsten Svan de Pol J(2023)Predicting Memory Demands of BDD Operations Using Maximum Graph CutsAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_4(72-92)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_4
Olliaro DBalbo GMarin ASereno M(2023)Skipping and Fetching: Insights on Non-conventional Product-Form SolutionsQuantitative Evaluation of Systems10.1007/978-3-031-43835-6_8(110-126)Online publication date: 20-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-43835-6_8
Khan SVolk MKatoen JBraibant ABouissou M(2021)Model Checking the Multi-Formalism Language FIGARO2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)10.1109/DSN48987.2021.00056(463-470)Online publication date: Jun-2021
https://doi.org/10.1109/DSN48987.2021.00056
Show More Cited By

Index Terms

Advanced features in SMART: the stochastic model checking analyzer for reliability and timing
1. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation
      2. Modeling methodologies
2. Mathematics of computing
  1. Probability and statistics
    1. Statistical paradigms
      1. Survival analysis
    2. Stochastic processes

Recommendations

SMART: The Stochastic Model checking Analyzer for Reliability and Timing
QEST '04: Proceedings of the The Quantitative Evaluation of Systems, First International Conference

SMART provides a seamless environment for the logic and probabilistic analysis of complex systems, for use in both the classroom and industrial applications.While initially designed as a powerful stochastic environment integrating multiple modeling ...
Tuning Temporal Features within the Stochastic π-Calculus

The stochastic \pi-calculus is a formalism that has been used for modeling complex dynamical systems where the stochasticity and the delay of transitions are important features, such as in the case of biochemical reactions. Commonly, durations of ...
Logic and stochastic modeling with SMART
Modelling techniques and tools for computer performance evaluation

We describe the main features of SMART, a software package providing a seamless environment for the logic and probabilistic analysis of complex systems. SMART can combine different formalisms in the same modeling study. For the analysis of logical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGMETRICS Performance Evaluation Review

ACM SIGMETRICS Performance Evaluation Review Volume 36, Issue 4

March 2009

68 pages

ISSN:0163-5999

DOI:10.1145/1530873

Issue’s Table of Contents

Copyright © 2009 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 March 2009

Published in SIGMETRICS Volume 36, Issue 4

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
134
Total Downloads

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

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sølvsten Svan de Pol J(2023)Predicting Memory Demands of BDD Operations Using Maximum Graph CutsAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_4(72-92)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_4
Olliaro DBalbo GMarin ASereno M(2023)Skipping and Fetching: Insights on Non-conventional Product-Form SolutionsQuantitative Evaluation of Systems10.1007/978-3-031-43835-6_8(110-126)Online publication date: 20-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-43835-6_8
Khan SVolk MKatoen JBraibant ABouissou M(2021)Model Checking the Multi-Formalism Language FIGARO2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)10.1109/DSN48987.2021.00056(463-470)Online publication date: Jun-2021
https://doi.org/10.1109/DSN48987.2021.00056
Giese HBlouin DAl-Ali RMkaouar HBandyopadhyay SIacono MAmrani MKlikovits SErata F(2021)An ontology for multi-paradigm modellingMulti-Paradigm Modelling Approaches for Cyber-Physical Systems10.1016/B978-0-12-819105-7.00009-X(67-122)Online publication date: 2021
https://doi.org/10.1016/B978-0-12-819105-7.00009-X
Kordon FHillah LHulin-Hubard FJezequel LPaviot-Adet E(2021)Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019International Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-021-00615-123:6(931-952)Online publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1007/s10009-021-00615-1
Isa MJawawi D(2018)A Methodology for Model-Based Reliability EstimationComputer Systems and Software Engineering10.4018/978-1-5225-3923-0.ch018(461-484)Online publication date: 2018
https://doi.org/10.4018/978-1-5225-3923-0.ch018
Klein JBaier CChrszon PDaum MDubslaff CKlüppelholz SMärcker SMüller D(2018)Advances in probabilistic model checking with PRISMInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0456-320:2(179-194)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10009-017-0456-3
Junges SKatoen JStoelinga MVolk M(2018)One Net Fits AllApplication and Theory of Petri Nets and Concurrency10.1007/978-3-319-91268-4_14(272-293)Online publication date: 24-Jun-2018
https://dl.acm.org/doi/10.1007/978-3-319-91268-4_14
Klein JBaier CChrszon PDaum MDubslaff CKlüppelholz SMärcker SMüller D(2016)Advances in Symbolic Probabilistic Model Checking with PRISMProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_20(349-366)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_20
Meijer JPol J(2016)Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability AnalysisProceedings of the 8th International Symposium on NASA Formal Methods - Volume 969010.1007/978-3-319-40648-0_20(255-271)Online publication date: 7-Jun-2016
https://dl.acm.org/doi/10.1007/978-3-319-40648-0_20
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.

Figures

Tables

Media

View Issue’s Table of Contents