草稿:Uppaal 模型檢查器

UPPAAL

開發者	Uppsala University Aalborg University
首次發佈	1995年 (1995)
程式語言	C++ and GUI in Java
作業系統	Linux Mac OS X Microsoft Windows
語言	English Danish Japanese Chinese Lithuanian
類型	Model checking
許可協議	Commercial Licenses Academic Licenses
網站	http://www.uppaal.org/ http://www.uppaal.com/

UPPAAL是一個用於對實時系統進行建模、確認和驗證的集成工具環境，該系統以時序自動機網絡為模型基礎，並擴展到幾種額外的數據類型（有界整數、數組等）。

自 1995 年發佈以來，它已在至少 17 個研究案例中使用，包括Lego Mindstorms 、飛利浦音頻協議和Mecel的變速箱控制器。

該工具是由瑞典烏普薩拉大學實時系統設計與分析小組和丹麥奧爾堡大學計算機科學基礎研究中心合作開發的。

有以下可用的擴展：

• Cora用於成本最優可達性分析。
• Tron用於在線測試實時系統（黑盒一致性測試）。
• 涵蓋COVERerage 最佳離線測試生成。
• Tiga用於基於時序遊戲 (TImed GAmes) 的控制器合成。
• 基於組件的定時系統的端口，利用偏序縮減技術。
• Pro用於概率可達性分析。 （已停止維護）
• SMC用於統計模型檢查。

外部連結

• UPPAAL 學術網站
• UPPAAL 商業網站
• 實時系統設計與分析組
• AAU 計算機科學系 DEIS 部門