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和内存泄漏。