SMART: The stochastic model checking analyzer for reliability and timing

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 formalisms, SMART now includes logical analysis and employs some of the most efficient data structures and algorithms for the analysis of discrete-state systems. For logical behavior explicit and symbolic state-space generation techniques and symbolic CTL modelchecking algorithms are available. For stochastic and timing behavior sparse-storage and Kronecker-based numerical solution approaches are available when the underlying process is a Markov chain, and discrete-event simulation is available for any type of underlying process. In addition, certain classes of non-Markov models can be solved numerically. For more details, see G. Ciardo et. al., "Logical and stochastic modeling with SMART", in Proc. Mod Tech. and Tools for Comp. Perf. Eval., LNCS 2794, Springer 2003, or the SMART User Manual available at http://www.cs.ucr.edu/-ciardo/SMART/.