The success of model checking and performance evaluation is due, in part, to the availability of tools to analyze systems. The tools that I have designed, helped to develop, or worked on implementing are listed below.
SMART, or Stochastic Model-checking Analyzer for Reliability and Timing, is a software package that allows models to be analyzed. Models may be specified either directly at a low level (e.g., as a finite state machine or Markov chain), or using a high-level formalism (e.g., as a Petri net). Analysis engines include CTL model checking and computation of performance measures.
MEDDLY, or Multi-terminal and Edge-valued Decision Diagram LibrarY, is an open-source software library for decision diagrams. It is written in C++ and has been integrated into several tools, including the new version of SMART. It is available from SourceForge (at the above link).