SMART: Stochastic Model-checking Analyzer for Reliability and Timing

Welcome to the new home for SMART, a software package to study complex discrete-state systems. Models may be specified either directly, as a finite state machine or Markov chain, or using a high-level formalism, such as a Petri net. Analysis engines include CTL model checking and computation of performance measures.

SMART is released under the Apache License, Version 2.0.