SMART: the stochastic model checking analyzer for reliability and timing
Gianfranco Ciardo, Andrew S. Miner · 2004
ii SmArT overview and organization of this User Manual The SmArT (Stochastic Model checking Analyzer for Reliability and Timing) tool is a software package to study complex discrete-state systems. With SmArT, it is possible to study the logical behavior of the system, by generating the state space underlying a complex model and asking temporal logic queries about its dynamic behavior, as done in traditional model-checking. Once one is satisfied that the logical behavior of the system is both correct and correctly captured by the model, performance, reliability, availability, and performability measures about the system can be computed with a large variety of state-of-the-art techniques. SmArT implements both numerical solution algorithms and discrete-event simulation techniques. These can be used in cooperation for the study of a complex system, since multiple interacting models are supported in a variety of ways, from a simple hierarchical solution of submodels to a built-in fixed-point iteration mechanism which may be used to perform sophisticated approximations. Numerical solution algorithms are provided not only for the widely-used class of models having an underlying continuous-time Markov chain, but also for the case where the underlying process is a discrete-time Markov chain, or, under certain conditions, even a Markov regenerative process arising from the use of both discrete and continuous phase-type distributions