跳至內容

英文维基 | 中文维基 | 日文维基 | 草榴社区

草稿: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的變速箱控制器。 [1]

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

有以下可用的擴展:

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

參考

[編輯]

外部連結

[編輯]