UPPAAL

UPPAAL是一個集成工具環境建模，確認和驗證建模為時間自動機的網絡，擴展數據類型（整數界，數組等）的實時系統。
UPPAAL CORA是UPPAAL的成本優化可達Anslysis一個分支由UPPAAL團隊為VHS和AMETIST項目的一部分開發的。而支持UPPAAL時間自動機的模型檢測，UPPAAL CORA使用時間自動機稱為LPTA的延伸。 LPTA允許你註釋模型與成本的概念。
這可以是延遲在某些情況下或特定行動的成本的成本。 UPPAAL CORA然後找到匹配的目標條件下的最佳路徑。
UPPAAL CORA已經使用在許多案例。其中一些網站的案例頁描述。如果你拿出有趣的用途，請與我們聯繫。我們有興趣聽你做什麼！
由於不同的內部數據結構，UPPAAL CORA目前由兩個不同版本的：
一個版本為最佳時間可達性分析的簡單情況。
一個版本的LPTA的滿語。
像UPPAAL，UPPAAL CORA是免費的，非營利性的使用，如評估，研究和教學目的。
這裡是“UPPAAL”的一些主要特點：
強大的
 
·UPPAAL CORA的建模語言是對變化建模的問題健壯。這意味著您在建模時的投資問題變化不丟失，因為它很容易適應現有的模式。
 
快
 
·雖然技術是相當新的，實驗性和從傳統業務研究使用的技術有很大不同，UPPAAL CORA是在一些案例中的競爭力。
 
兼容
 
·UPPAAL CORA的語言是UPPAAL的一個超集。任何有效的UPPAAL模式也是一個有效的UPPAAL CORA模型。這使得它很容易和方便地重用和調整現有的模型UPPAAL CORA。
 
當前
 
·UPPAAL CORA是基於UPPAAL的最新內部開發版本，包含了最新的性能和語言的改進。然而一個實驗性的工具，缺少許多UPPAAL的驗證功能。
局限性：
UPPAAL CORA全LPTA載體具有許多限制。這些限制不是根本的，但是使用新的內部數據結構與功能集目前僅限的結果。隨著時間的推移，這些限制將得到解決。
- 無外推，因此終端無法保證，除非你保證，無論是：
·該系統是無環。
·所有的時鐘都被不變界。
- 只有簡單的可達性：
·無活動性檢查
·無死鎖檢查
- 有限使用的指導：
·支持（成本+剩餘）排序實現（最好先搜索）
·支持啟發式變量實現，但表達式不能引用成本變量。
什麼是新的，在此版本：
·該版本修正了崩潰的bug和內存洩漏。