UPPAAL 2987修订版4.0.6_Uppaal 4.0.6 Rev 2987下载地址

集成工具环境建模，验证和验证实时系统

实时系统

使用UPPAAL时间自动机的网络模型，扩展的数据类型（数组，有限的整数等）。

该工具在丹麦的奥尔堡大学，瑞典乌普萨拉大学的信息技术和计算机科学系部之间的神器出山:www.shenqi73.com合作开发。

UPPAAL是适当的系统，可以作为一个集合的不确定性的过程，有限的控制结构和实际值的时钟模型，通过渠道或共享变量WPD94的沟通，LPW97b。

典型的应用领域包括实时控制器和通信协议，尤其是那些在计时方面是至关重要的。

UPPAAL由三个主要部分组成：描述语言，仿真和模型检查。的描述语言是一种非确定性的数据类型（例如，有界的整数，阵列等）保护命令语言。

UPPAAL作为一个模型或设计的语言来描述系统的行为，如网络自动延长时钟和数据变量。该模拟器是一种验证工具，使系统在早期的设计（或模型）的阶段可能出现的动态执行检查，从而提供了一种廉价的平均故障检测之前，验证它涵盖了详尽的动态行为的系统的模型检查。

模型检查器可以检查的不变和可达性物业的探索系统的状态空间，象征性的国家为代表的约束条款，即可达性分析。

的两个主要的设计标准，工具Uppaal的使用效率和易用性。上的动态搜索技术中的应用一直UPPAAL模型检查器的效率的关键。

另外一个重要的关键，效率是一个象征性的应用技术，减少验证问题的有效的操作和解决的约束[WPD94，LPW95c，LLPW97，BLPWW99]。

为了便于建模和调试，UPPAAL模型检查器可能会自动生成一个诊断跟踪，解释了为什么一个属性是由系统描述（或不）满意。

诊断的模型检查器所产生的痕迹，可以自动加载到模拟器，它可以用于可视化的跟踪和调查。

UPPAAL已被应用在大量的案例研究（参见案例部分）。为了满足需求而产生的案例研究，该工具已被延长的各种功能。

当前版本的UPPAAL称为Uppaal2k的，1999年9月首次发布。这是客户端/服务器应用程序在Java和C + +，是目前可用于Linux，SunOS和Windows 95/98/NT中。

下面是一些主要特点“工具Uppaal”：

·图形化的系统编辑器，让系统的图形化描述。
·A的图形模拟器，提供图形可视化和记录的系统描述可能的动态行为，即序列符号的系统状态。它也可以用于可视化的模型检查器所产生的痕迹。由于3.4版本的模拟器可以看到一个跟踪的消息序列图（MSC）。
·需求规格说明书的编辑器，也构成了图形用户界面的验证者Uppaal2k。
·A模型检查器自动验证的安全性和保税活动属性的符号状态空间的可达性分析。自3.2版本，它也可以检查活动属性。
·生成一个特定的实时系统的验证的情况下的诊断跟踪失败。诊断跟踪可能会自动加载，并以图形可视化模拟器。自3.4版本，它可以指定生成的跟踪应该是最短或最快的。


注：UPPAAL工具，在学术界和私人的非商业应用是免费的。对于商业应用需要一个商业许可。

此版本中的新功能：

·新的主要版本的UPPAAL。注意，GUI需要Java 5版。
·请注意，这个版本包含的语法的变化，你将需要转换你的老款车型。
·二进制文件的Mac OS X下载（需要的MacOS 10.4 - 被称为老虎 - Java 5中是不可用的早期版本）。