草稿:Uppaal 模型檢查器
UPPAAL是一個用於對實時系統進行建模、確認和驗證的集成工具環境，該系統以時序自動機網絡為模型基礎，並擴展到幾種額外的數據類型（有界整數、數組等）。
自 1995 年發佈以來，它已在至少 17 個研究案例中使用，包括Lego Mindstorms 、飛利浦音頻協議和Mecel的變速箱控制器。 [1]
該工具是由瑞典烏普薩拉大學實時系統設計與分析小組和丹麥奧爾堡大學計算機科學基礎研究中心合作開發的。
有以下可用的擴展：
- Cora用於成本最優可達性分析。
- Tron用於在線測試實時系統（黑盒一致性測試）。
- 涵蓋COVERerage 最佳離線測試生成。
- Tiga用於基於時序遊戲 (TImed GAmes) 的控制器合成。
- 基於組件的定時系統的端口，利用偏序縮減技術。
- Pro用於概率可達性分析。 （已停止維護）
- SMC用於統計模型檢查。