Gianfranco Ciardo
Skip Abstract Section
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.
- 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. Google Scholar
Digital Library
- A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS, pages 193--207. Springer-Verlag, 1999. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- H. Choi, V.G. Kulkarni, and K.S. Trivedi. Markov regenerative stochastic Petri nets. In Performance '93. North-Holland, Sept. 1993. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- G. Ciardo and C. Lindemann. Analysis of deterministic and stochastic Petri nets. In Proc. PNPM, pages 160--169, Oct. 1993. IEEE CS Press.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 1999. Google ScholarDigital Library
- P. Fernandes, B. Plateau, and W.J. Stewart. Efficient descriptor-vector multiplication in stochastic automata networks. J. ACM, 45(3):381--414, 1998. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- A.S. Miner. Efficient solution of GSPNs using canonical matrix diagrams. In Proc. PNPM, pages 101--110, Sept. 2001. IEEE CS Press. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- B. Plateau. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In Proc. SIGMETRICS, pages 147--153, May 1985. Google ScholarDigital Library
- W.J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.Google Scholar
- 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. Google ScholarDigital Library
- M. Wan and G. Ciardo. Symbolic reachability analysis of integer timed Petri nets. In Proc. SOFSEM, Jan. 2009. Springer-Verlag. To appear. Google ScholarDigital Library
- M. Wan, G. Ciardo, and A.S. Miner. Decision-diagram-based approximate steady-state analysis of large structured Markov models. In preparation.Google Scholar
- 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. Google ScholarDigital Library
Index Terms
- Advanced features in SMART: the stochastic model checking analyzer for reliability and timing
Recommendations
SMART: The Stochastic Model checking Analyzer for Reliability and Timing
QEST '04: Proceedings of the The Quantitative Evaluation of Systems, First International ConferenceSMART 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 evaluationWe 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