Uppaal モデルチェッカー

UPPAALは、時間付きオートマトンネットワークとしてモデル化されたリアルタイムシステムのモデリング、検証、妥当性確認を行うための統合ツール環境であり、データ型（境界付き整数、配列など）で拡張されています。

1995年の発売以来、レゴ マインドストーム、フィリップスのオーディオ プロトコル、メセルのギアボックス コントローラーなど、少なくとも17の事例研究で使用されています。^{[ 1 ]}

このツールは、スウェーデンのウプサラ大学のリアルタイムシステム設計・分析グループと、デンマークのオールボー大学のコンピュータサイエンス基礎研究グループとの共同開発によって誕生しました。

利用可能な拡張機能は以下のとおりです。

• コスト最適到達可能性分析のためのCora 。
• Tronは、リアルタイムシステムのオンラインテスト（ブラックボックス適合性テスト）に使用できます。
• カバー画像は、カバレッジ最適化オフラインテスト生成のために、 2021年1月17日にWayback Machineにアーカイブされました。
• Tigaは、Timed Games（TIMED GAmes）向けのコントローラー合成ソフトウェアです。
• 部分順序削減技術を活用した、コンポーネントベースの時間制御システム向け移植版。
• 確率的到達可能性分析のためのPro版。（販売終了）
• SMCは統計モデル検査のための略語です。

• UPPAAL学術ウェブサイト
• UPPAALの商用ウェブサイト
• リアルタイムシステムの設計と解析グループ
• AAUコンピュータサイエンス学科DEISユニット