SMART: stochastic model-checking analyzer for reliability and timing

SMART is a software package integrating logic and stochastic modeling formalisms into a single environment. Models expressed in different formalisms can be combined in the same study. To study logical behavior, both explicit and symbolic state-space generation techniques, as well as CTL model-checking algorithms, are available. To study stochastic and timing behavior, both explicit and Kronecker-based numerical solution approaches are available. Since SMART is intended as an industry and research tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.