お勧めのモデル検査・形式手法を教えてください。

SPIN,NuSMV,LTSAやVDM,...と色々ありますが、
1)今後、一番普及しそうなもの
2)状態遷移図がかけてグラフィカルで扱いやすく、文法も覚えやすく簡単に扱えて仕様の検討からデバッグにまで使えるもの


といったらそれぞれ何になると思われますか？