スウェーデンのUppsala大学とデンマークのAalbog大学の共同プロジェクトです。
営利目的の場合は、許可が必要です。（営利目的の定義は？）
状態遷移に時間オートマトンを付加した、モデルでの検証を行うツールです。

GUI入力による、モデル検査が可能です。
以前、NSADA(現JAXA)で、SELENEのIV&Vに使用した実績があったと思います。
CoVerというテストケース作成ツールもあります。

http://www.uppaal.com/

チュートリアル（日本語）
http://www.it.uu.se/research/group/darts/uppaal/tu...