草稿:Uppaal模型檢查器
 | 本草稿尚未提交審核
提交前，請先查閱維基百科不是什麼，以免犯下常見錯誤。 要讓草稿被接受，需要至少滿足以下要求：
我們強烈不鼓勵您創建與您自己、您所在的組織、其對手或其產品相關的條目。如果您仍要這麼做，請申報利益衝突。 注意：若您提交之後，本模板出現在頁面最下方，表示您已成功提交。
如何改善您的草稿
|  |
UPPAAL是一個用於對實時系統進行建模、確認和驗證的集成工具環境，該系統以時序自動機網絡為模型基礎，並擴展到幾種額外的數據類型（有界整數、數組等）。
自 1995 年發佈以來，它已在至少 17 個研究案例中使用，包括Lego Mindstorms 、飛利浦音頻協議和Mecel的變速箱控制器。 [1]
該工具是由瑞典烏普薩拉大學實時系統設計與分析小組和丹麥奧爾堡大學計算機科學基礎研究中心合作開發的。
有以下可用的擴展：
- Cora用於成本最優可達性分析。
- Tron用於在線測試實時系統（黑盒一致性測試）。
- CoVer 最佳離線測試生成。
- Tiga用於基於時序遊戲 (TImed GAmes) 的控制器合成。
- 基於組件的定時系統的 port，利用偏序縮減技術。
- Pro 用於概率可達性分析。 （已停止維護）
- SMC用於統計模型檢查。