Uppaal モデルチェッカー

UPPAAL は、データ型(制限付き整数、配列など) で拡張された、タイムド オートマトンネットワークとしてモデル化されたリアルタイムシステムのモデリング、検証、および確認を行う統合ツール 環境です。

1995年のリリース以来、Lego Mindstorms、Philipsオーディオプロトコル、Mecelのギアボックスコントローラーなど、少なくとも17のケーススタディで使用されています。^[1]

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

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

• コスト最適到達可能性分析のためのCora。
• リアルタイム システムをオンラインでテストするためのTron (ブラック ボックス適合テスト)。
• COVERerage に最適なオフライン テスト生成のカバー。
• TImed ゲーム ベースのコントローラー合成用のTiga 。
• 部分順序削減技術を活用したコンポーネント ベースのタイミング システム用のポート。
• 確率的到達可能性分析のPro 。(廃止)
• 統計モデル検査のためのSMC。

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